[
  "\"ÌÊÖ›[Äàt‚ÕÆ…ýÓ²",
  [
    [
      "Vale.Bignum.X64.va_quick_Adcx_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "2a5cc8a65f0733cf6205de250b9c5e1e"
    ],
    [
      "Vale.Bignum.X64.va_quick_Adox_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "848432381ac1e09d7726da41a3936f29"
    ]
  ]
]