Revision 1539fc67ec7cd1f092967452d8ae47d170ca149b authored by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC, committed by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC
1 parent 56130dc
Vale.X64.State.fsti.hints
[
"@\rn\n�\u0016/��\u0002/0QE\u0006�",
[
[
"Vale.X64.State.eval_reg_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"edbf98f7789b3bdd3b611d64f58d9e0a"
],
[
"Vale.X64.State.eval_reg_xmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"e7ec6530bfea107702888ffb9b41b95e"
],
[
"Vale.X64.State.eval_maddr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"disc_equation_Vale.X64.Machine_s.MIndex",
"disc_equation_Vale.X64.Machine_s.MReg",
"fuel_guarded_inversion_Vale.X64.Machine_s.maddr"
],
0,
"41b9709bfe3741d4bdb5c68ced6ae855"
],
[
"Vale.X64.State.eval_operand",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"f6763bbdb3d6a3c9eaa1ed510a837cca"
],
[
"Vale.X64.State.eval_operand128",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"639aa7d803477464a88596b3cdb4feaf"
],
[
"Vale.X64.State.update_reg_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"ef087aac478bc2f0c169e48efd5a005f"
],
[
"Vale.X64.State.update_reg_xmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"bf51f7c3e1583b04b05075ae5b70c496"
],
[
"Vale.X64.State.valid_src_operand",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"07c8728a5f0a3082da0519dc4b116e0b"
],
[
"Vale.X64.State.valid_src_operand128",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"f53e5524f14b1a602a4b1f22ffc96b99"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...