[
  "�\u0015P��f��m�B��I�J",
  [
    [
      "Vale.AES.X64.AESCTRplain.va_lemma_Aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_dff147d5c995aa65a971b362dbc2897b"
      ],
      0,
      "3d9783d902e5a5fdc84b25035455f83d"
    ],
    [
      "Vale.AES.X64.AESCTRplain.va_wp_Aes_counter_loop",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "15ad3e00bcdaaae8d22e1e77bb9c3654"
    ],
    [
      "Vale.AES.X64.AESCTRplain.va_quick_Aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "51617546c7a2b82c2b88d422528ee6e9"
    ]
  ]
]