[
  "å¨R\u0003µG*\u0019Y\u0006Š¸]\u001a­Ú",
  [
    [
      "Lib.Loops.for",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0e406ebb8fe1da55578bcffeb79cfd32",
        "refinement_interpretation_Tm_refine_427ccb352453c408ac8eeec6c2c8abc6",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d2c47292ec0e1061d3ad1f91c03f01aa"
    ],
    [
      "Lib.Loops.while",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb"
      ],
      0,
      "ad7751fb730e6c9eebc23dd2d4229a2c"
    ]
  ]
]