[
  ".�h���Ȳ\u0010\"�\u0000eS:",
  [
    [
      "Vale.Test.X64.Vale_memcpy.va_req_Memcpy",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "a302c9bd2f225a4757685bd00496b5a5"
    ],
    [
      "Vale.Test.X64.Vale_memcpy.va_ens_Memcpy",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.X64.Decls.va_state_eq",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "043ffc8e7689889019c648a06381aae5"
    ],
    [
      "Vale.Test.X64.Vale_memcpy.va_quick_Memcpy",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "b3f0a725e53f80063fdba1a34219dcce"
    ]
  ]
]