[
  "�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,
      "4ee16ea32975dd8c303801faee7eeb0f"
    ],
    [
      "Lib.Loops.while",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b16bf82b210653a34e4d7322fab91ffb"
      ],
      0,
      "7a7f0e3dc44fe8e1a59a37512f249db1"
    ]
  ]
]