Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Vale.X64.Machine_s.fst.hints
[
"TK��w\u0010��y�\u0019ԙ@(�",
[
[
"Vale.X64.Machine_s.int_to_nat64",
1,
1,
0,
[
"@query", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"efe8c657742ed53e62079b5db8551637"
],
[
"Vale.X64.Machine_s.n_regs",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"e346a92a5e5b7b894c54500348ecc5b7"
],
[
"Vale.X64.Machine_s.t_reg_file",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"c399eec7c842e3248abfb98893b21efb"
],
[
"Vale.X64.Machine_s.reg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"7ffac863d41888b70a29dc3c72bd72d9"
],
[
"Vale.X64.Machine_s.__proj__Reg__item__r",
1,
1,
0,
[
"@query", "proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.Machine_s.Reg_rf"
],
0,
"1ad44f02ad73cc1448fe93131993eb41"
],
[
"Vale.X64.Machine_s.t_reg_to_int",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.t_reg_file", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"612f4036bbd61c1d94df748e61c9f84a"
],
[
"Vale.X64.Machine_s.maddr",
1,
1,
0,
[ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
0,
"e76d4dd7b9f81841687bc8cded08323a"
],
[
"Vale.X64.Machine_s.__proj__MConst__item__n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba45d2688e3fd04e2e5908c939c77b9a"
],
0,
"f78768de37ba7df6085ac797a07eb58e"
],
[
"Vale.X64.Machine_s.__proj__MReg__item__r",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c60fc719647aa74bcc3bff5ee709f429"
],
0,
"700c6a6354aa8e76686487d24b81048d"
],
[
"Vale.X64.Machine_s.__proj__MReg__item__offset",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c60fc719647aa74bcc3bff5ee709f429"
],
0,
"9620ec1be67c4cdb74ab5b230c14b106"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__base",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"9e0235dd2f267db08ebb024948f29fc0"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__scale",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"a3884785d4bebda0d4e2dc02af2757c4"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__index",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"01c09fd695b37f9f14d4b40e24bdbbd9"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__offset",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"6283a451cf09f85f378b9ca8a94cf1d2"
],
[
"Vale.X64.Machine_s.tmaddr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
"assumption_Vale.Arch.HeapTypes_s.taint__uu___haseq",
"assumption_Vale.X64.Machine_s.maddr__uu___haseq",
"equation_Prims.eqtype", "kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.X64.Machine_s.maddr@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"3b25de8969f8b2f4e99fb4b45cd16a18"
],
[
"Vale.X64.Machine_s.operand",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
"assumption_Vale.Arch.HeapTypes_s.taint__uu___haseq",
"assumption_Vale.X64.Machine_s.maddr__uu___haseq",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.eqtype", "equation_Vale.X64.Machine_s.tmaddr",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.X64.Machine_s.maddr@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"be6538d5a9b8748f22f9c23bbcad8276"
],
[
"Vale.X64.Machine_s.__proj__OConst__item__n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_db12994d84d9b6d7c0660d6d33952e45"
],
0,
"d194d437efa54e1f74baab1daa374de8"
],
[
"Vale.X64.Machine_s.__proj__OReg__item__r",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440"
],
0,
"893ec3cd235b66f2ec4f1c83414ff47c"
],
[
"Vale.X64.Machine_s.__proj__OMem__item__m",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OMem",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_12d7e4741e449358bfb593c2d177b831"
],
0,
"df4989169722b8022c99a9efaa88ccb5"
],
[
"Vale.X64.Machine_s.__proj__OStack__item__m",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OStack",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba9505ad2c29cc6490e2327dd9964a3e"
],
0,
"0a4da16f679e3227491249a2ffffa2db"
],
[
"Vale.X64.Machine_s.operand_rf",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg_file",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32"
],
0,
"1550f918c8b7f8d376e766210c5abd98"
],
[
"Vale.X64.Machine_s.oreg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg_file",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"4581f360f7301584b0cfdab4c7a2d684"
],
[
"Vale.X64.Machine_s.reg_Rax",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"b503ee73bc68cadde115a2c5eb6407ee"
],
[
"Vale.X64.Machine_s.reg_Rbx",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"fe95513b5f0e5643d72d849bfa350c49"
],
[
"Vale.X64.Machine_s.reg_Rcx",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"02a8eea2da1abcfaa4dece344027bcbe"
],
[
"Vale.X64.Machine_s.reg_Rdx",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"6c1ae88aedbf138699dd2a7fab21b428"
],
[
"Vale.X64.Machine_s.reg_Rsi",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"d13d9f1e220b2a8f9b6b519357ae3080"
],
[
"Vale.X64.Machine_s.reg_Rdi",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"fcfc3006d8d2e97f09a1eb1450543a6b"
],
[
"Vale.X64.Machine_s.reg_Rbp",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"dc1e3f13fc689edb598da34b917a26b1"
],
[
"Vale.X64.Machine_s.reg_Rsp",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"0e0c5786ea091f535ce5234478306b52"
],
[
"Vale.X64.Machine_s.reg_R8",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"7eb8983753d17cc171774b20d30993ce"
],
[
"Vale.X64.Machine_s.reg_R9",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"29ecea14883e2e8cf0a3a5ed64404d93"
],
[
"Vale.X64.Machine_s.reg_R10",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"e7ba7399a16c6992507f59d29b3fb95e"
],
[
"Vale.X64.Machine_s.reg_R11",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"b410884d1086e409885f70a747a82549"
],
[
"Vale.X64.Machine_s.reg_R12",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"0193898970f1bf2cceb26e69e872bf2d"
],
[
"Vale.X64.Machine_s.reg_R13",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"e2172ddf0389fe3e166056e32d139b3d"
],
[
"Vale.X64.Machine_s.reg_R14",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"f73502889fd2758f41ea2d74c3d8f8cb"
],
[
"Vale.X64.Machine_s.reg_R15",
1,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"613d66f0f1a5d6657333f5248469bf94"
],
[
"Vale.X64.Machine_s.operand64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"166a42fad6aca955ac1806e3f2691239"
],
[
"Vale.X64.Machine_s.operand128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d94d4fe49bfe40cb65300e0536d3f7b4"
],
[
"Vale.X64.Machine_s.__proj__Ins__item__ins",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.Ins",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_bf287cd7801c59db9c693887788476a6"
],
0,
"73090a7f7ef1b5d31b5539d9cb58b77e"
],
[
"Vale.X64.Machine_s.__proj__Block__item__block",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.Block",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a7bbfd6b3498c17c8d1674fce71b8656"
],
0,
"c453c5ccf4c4d1366552fa0693469bfb"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifCond",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"4bcbec0a04d992e755e4b63b01e91939"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifTrue",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"c0a926ee68cdba20dc1b57b864c6fea6"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifFalse",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"bab694a57ebee37a7df09041c331b6c4"
],
[
"Vale.X64.Machine_s.__proj__While__item__whileCond",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.While",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b"
],
0,
"c3a00b3bc961209a44263164888ad3d3"
],
[
"Vale.X64.Machine_s.__proj__While__item__whileBody",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.While",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b"
],
0,
"a6409a2d0e1d26d89c45ef04489a715c"
],
[
"Vale.X64.Machine_s.__proj__BranchPredicate__item__pred",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.BranchPredicate",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_665855d5d2c2e8d0f359546a27d4e0a8"
],
0,
"55a5a2ef1c27afe308b8a4406cde458e"
],
[
"Vale.X64.Machine_s.__proj__MemAccess__item__addr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MemAccess",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9314f39e5dace3fd827ffe198da8b3c3"
],
0,
"6b8eb5781545f964d141cfbeb48f6dd9"
],
[
"Vale.X64.Machine_s.int_to_nat64",
2,
1,
0,
[
"@query", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"d2cdd913adf7b58864a7a14c8cf4d220"
],
[
"Vale.X64.Machine_s.n_regs",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"e2266b576c5a9bb323cc63ff094190ec"
],
[
"Vale.X64.Machine_s.t_reg_file",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"8269e8fc2729a5d81899b4cbc84f0b46"
],
[
"Vale.X64.Machine_s.reg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"b710dd5170e6f74aeb80f3a423d3673f"
],
[
"Vale.X64.Machine_s.__proj__Reg__item__r",
2,
1,
0,
[
"@query", "proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_Vale.X64.Machine_s.Reg_rf"
],
0,
"fa0dd972bd04d9a3e69d73f51d9c541f"
],
[
"Vale.X64.Machine_s.t_reg_to_int",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.t_reg_file", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64"
],
0,
"8ee275c9746770fe21d59d4104480103"
],
[
"Vale.X64.Machine_s.maddr",
1,
1,
0,
[ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
0,
"397b98c744e80f7955e8d9949fe85e5b"
],
[
"Vale.X64.Machine_s.__proj__MConst__item__n",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba45d2688e3fd04e2e5908c939c77b9a"
],
0,
"fd3fe0f940c679f7a3dcd2a3b9c957b9"
],
[
"Vale.X64.Machine_s.__proj__MReg__item__r",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c60fc719647aa74bcc3bff5ee709f429"
],
0,
"0c07cf13bafa9f48c5c5ed86cc297f85"
],
[
"Vale.X64.Machine_s.__proj__MReg__item__offset",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c60fc719647aa74bcc3bff5ee709f429"
],
0,
"6009f5b700f021842668b141e52108d0"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__base",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"5362852f47a832e5f1aa138e3261e27c"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__scale",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"69e47448819c9a9fa0a1f7eb53cea91e"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__index",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"2abb8a8cae36abf17afe393545d37318"
],
[
"Vale.X64.Machine_s.__proj__MIndex__item__offset",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MIndex",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_7355595e080da4f6c86cbe87ff8f3f86"
],
0,
"56ceae45a4f8aab1300d81428647ac44"
],
[
"Vale.X64.Machine_s.tmaddr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
"assumption_Vale.Arch.HeapTypes_s.taint__uu___haseq",
"assumption_Vale.X64.Machine_s.maddr__uu___haseq",
"equation_Prims.eqtype", "kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.X64.Machine_s.maddr@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"ddcebf55add03f250a9f993ff86ba73b"
],
[
"Vale.X64.Machine_s.operand",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"assumption_FStar.Pervasives.Native.tuple2__uu___haseq",
"assumption_Vale.Arch.HeapTypes_s.taint__uu___haseq",
"assumption_Vale.X64.Machine_s.maddr__uu___haseq",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.eqtype", "equation_Vale.X64.Machine_s.tmaddr",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"kinding_Vale.X64.Machine_s.maddr@tok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"9ce4147fcc05a29535332eba878352e6"
],
[
"Vale.X64.Machine_s.__proj__OConst__item__n",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_db12994d84d9b6d7c0660d6d33952e45"
],
0,
"4d46aa93c3882c32fb71a9f213c6fabd"
],
[
"Vale.X64.Machine_s.__proj__OReg__item__r",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_e7e8c9464c24212d7cc1d1b3047a8440"
],
0,
"7ecbd59258777447ea256a55c6b13b84"
],
[
"Vale.X64.Machine_s.__proj__OMem__item__m",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OMem",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_12d7e4741e449358bfb593c2d177b831"
],
0,
"ad98c6d14c89ab98fe7b83f5e6bad1ae"
],
[
"Vale.X64.Machine_s.__proj__OStack__item__m",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OStack",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_ba9505ad2c29cc6490e2327dd9964a3e"
],
0,
"08d8278f5b7762c18d2c6f15ee9e60e7"
],
[
"Vale.X64.Machine_s.operand_rf",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg_file",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32"
],
0,
"aca4fb8e683af19cc0999520c5a1a91a"
],
[
"Vale.X64.Machine_s.oreg",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg_file",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.int",
"haseqTm_refine_0559236e7a05befcc7b6302f3642ad81",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"a1b3fb3aa0cebcbe31b07811d1e6b8ca"
],
[
"Vale.X64.Machine_s.reg_Rax",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"b204ffcd556c8598bfc60ae116ca1f52"
],
[
"Vale.X64.Machine_s.reg_Rbx",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"d3951ecffee249e70a73d2fb9e2a9779"
],
[
"Vale.X64.Machine_s.reg_Rcx",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"83cf54e473f8e301a06e0e8ef2e82ed8"
],
[
"Vale.X64.Machine_s.reg_Rdx",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"70ec8280016082b1e30bb2e3eee15d4d"
],
[
"Vale.X64.Machine_s.reg_Rsi",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"1c5dd778714eaed2ef4d9304b4f6fe4e"
],
[
"Vale.X64.Machine_s.reg_Rdi",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"36aed302156313ee7ab311051092a427"
],
[
"Vale.X64.Machine_s.reg_Rbp",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"2f1869e4436d9e98619820e575d31f65"
],
[
"Vale.X64.Machine_s.reg_Rsp",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"5873d129c9c89dedf00768a1e3634320"
],
[
"Vale.X64.Machine_s.reg_R8",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"9b3bf252768b7e80bd51cf7802ca06cc"
],
[
"Vale.X64.Machine_s.reg_R9",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"f4f9d07523f46a06f09668755395b9d8"
],
[
"Vale.X64.Machine_s.reg_R10",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"918040249c9ea513cdbed963aa525454"
],
[
"Vale.X64.Machine_s.reg_R11",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"ecb8ead04a6a590bcf7cc280fca9fd2a"
],
[
"Vale.X64.Machine_s.reg_R12",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"670aa4835165ce80e8d02ffb3fbb065e"
],
[
"Vale.X64.Machine_s.reg_R13",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"2d3ab2b230b14aec99139d7e4407ed35"
],
[
"Vale.X64.Machine_s.reg_R14",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"f0fcbf4d987f60a58f010f44aced001f"
],
[
"Vale.X64.Machine_s.reg_R15",
2,
1,
0,
[
"@query", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"projection_inverse_BoxInt_proj_0"
],
0,
"1e0c1c9e7e93043b1a253a1fb9eeceb6"
],
[
"Vale.X64.Machine_s.operand64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"66e390766c2f66d13689ca841d8966f6"
],
[
"Vale.X64.Machine_s.operand128",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"455b8d6bcd35c7a895a2b6a9093a0383"
],
[
"Vale.X64.Machine_s.__proj__Ins__item__ins",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.Ins",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_bf287cd7801c59db9c693887788476a6"
],
0,
"19c5566ddafd442bbb72a57000dab626"
],
[
"Vale.X64.Machine_s.__proj__Block__item__block",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.Block",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a7bbfd6b3498c17c8d1674fce71b8656"
],
0,
"84357743415c98323f2f01966cd99bb1"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifCond",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"4e5ca238dd1249485f9745506c19fa7d"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifTrue",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"ad3a53cf88a21c51126409cb787c165b"
],
[
"Vale.X64.Machine_s.__proj__IfElse__item__ifFalse",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.IfElse",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_936e87655f3f541d857ac072da8c1df0"
],
0,
"c6523ff959c5adbcb1c563992e88db7c"
],
[
"Vale.X64.Machine_s.__proj__While__item__whileCond",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.While",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b"
],
0,
"6f137208055316bc40249a919f449a0c"
],
[
"Vale.X64.Machine_s.__proj__While__item__whileBody",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.While",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b"
],
0,
"a62a59958cef4e84fd6dee711f0ebd6e"
],
[
"Vale.X64.Machine_s.__proj__BranchPredicate__item__pred",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.BranchPredicate",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_665855d5d2c2e8d0f359546a27d4e0a8"
],
0,
"55cae4b469c727ee582c0081a3110398"
],
[
"Vale.X64.Machine_s.__proj__MemAccess__item__addr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MemAccess",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9314f39e5dace3fd827ffe198da8b3c3"
],
0,
"28c2db05872066d87d152808cf3db30e"
]
]
]
Computing file changes ...
