[
  "گ�\u001ext\u00162�!��SD�",
  [
    [
      "X64.Vale.State.eval_maddr",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_X64.Machine_s.MConst",
        "disc_equation_X64.Machine_s.MIndex",
        "disc_equation_X64.Machine_s.MReg",
        "fuel_guarded_inversion_X64.Machine_s.maddr"
      ],
      0,
      "c91d5ee465a6d03890227f0099b285da"
    ],
    [
      "X64.Vale.State.to_nat64",
      1,
      1,
      0,
      [
        "@query", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "d924e1334aa69c5e356b4e75d49ceeb1"
    ],
    [
      "X64.Vale.State.eval_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_X64.Machine_s.OConst",
        "disc_equation_X64.Machine_s.OMem",
        "disc_equation_X64.Machine_s.OReg",
        "fuel_guarded_inversion_X64.Machine_s.operand"
      ],
      0,
      "4795c45689acb232724e928bc98f39ef"
    ],
    [
      "X64.Vale.State.update_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_X64.Machine_s.OConst",
        "disc_equation_X64.Machine_s.OMem",
        "disc_equation_X64.Machine_s.OReg",
        "fuel_guarded_inversion_X64.Machine_s.operand"
      ],
      0,
      "b23b4990c6e8177332727b04e0eb804c"
    ],
    [
      "X64.Vale.State.valid_operand",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_X64.Machine_s.OConst",
        "disc_equation_X64.Machine_s.OMem",
        "disc_equation_X64.Machine_s.OReg",
        "fuel_guarded_inversion_X64.Machine_s.operand"
      ],
      0,
      "a6f79c702da10674b25ee6b963fd17f9"
    ]
  ]
]