[
  "Ça”\u000ehÆ2”\u0017˜âm†\u0012~\u0010",
  [
    [
      "Vale.X64.Stack.va_quick_Callee_save_registers",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "55bdf49d606c45a8d5228cdc70078688"
    ],
    [
      "Vale.X64.Stack.va_quick_Callee_restore_registers",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "0b06103ca7eb1afa19fc45181d6c2794"
    ]
  ]
]