[
  "\u0017��\bRgݧ�FJ�D4�\u0010",
  [
    [
      "Spec.Salsa20.Test.test_quarter_round",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8a02b4ab6296b3a91d7a37757186265d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e351e5d087806c75d123854cea4f0d82",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c79803890910bb12ebc1a1c4bcbcbead"
    ],
    [
      "Spec.Salsa20.Test.test_row_round",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.min_int",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_28dc4c27ed07dfd7c8c66c674e5d7be1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_85d9ba499a9148547205faf6bcb50ea3",
        "refinement_interpretation_Tm_refine_c91ae56ff6de446e4a00ac265e32a3d4",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_dae2272c5575f12fee0fbfd7bbaf4b4c",
        "refinement_interpretation_Tm_refine_f9afaa2f85e7272daeacbebc02445c9b",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "229a33e6aa257d5b94f96075fa394e75"
    ],
    [
      "Spec.Salsa20.Test.test_column_round",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.min_int",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_28dc4c27ed07dfd7c8c66c674e5d7be1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5be0e76c269b23ec4dcffe3ae35e1a91",
        "refinement_interpretation_Tm_refine_85d9ba499a9148547205faf6bcb50ea3",
        "refinement_interpretation_Tm_refine_c91ae56ff6de446e4a00ac265e32a3d4",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_dae2272c5575f12fee0fbfd7bbaf4b4c",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4beae7103d50eb1244851b506044c7d6"
    ],
    [
      "Spec.Salsa20.Test.test_column_round2",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2c48eb1e83bf3aae41f475e2badbe634",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a91af992cbd627442133ef638bceea52"
    ],
    [
      "Spec.Salsa20.Test.test_salsa20_core",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.UInt.min_int", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_034a06ffa3eadc39e3e92192e2ee04f1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a2ef91ff46dd2092c42501f4f9528acd",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "1cfc19a7eb70c3c1bcf1dc2da49e3e08"
    ]
  ]
]