[
  "ªeiTË‘«Zf1)\u0015^Ûžî",
  [
    [
      "Test.NoHeap.test_many",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
        "refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v"
      ],
      0,
      "badf5b320df020a976ad21a2ce366b06"
    ]
  ]
]