[
  "�\u0011Xՠ(���]���\u0016k�",
  [
    [
      "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,
      "f49b94a01e2246eb6002d7d4a802c0d6"
    ],
    [
      "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,
      "b111fcd8a17c989206a2fa946404c0dd"
    ],
    [
      "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,
      "1a9224c2184b5a24ff7b6eb8cb873257"
    ],
    [
      "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,
      "df094197264bf6baac01df6c88a4a8ec"
    ],
    [
      "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,
      "79bbf12c48a40207516c299a8bb65a8a"
    ],
    [
      "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,
      "83ce804d5ed7f99b33dd4067f59967f4"
    ],
    [
      "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,
      "1962c0a945b4d37ac413756351854070"
    ],
    [
      "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,
      "97aa57225245fece8518f3fc48b4db18"
    ],
    [
      "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,
      "03e8f046c6e747fcd4af7465494bf943"
    ]
  ]
]