[
  ";‘TúÃ*©“.Q«5øRà\r",
  [
    [
      "Hacl.Hash.PadFinish.pad_len",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "89512fa93b26014d6ef28320471d1378"
    ]
  ]
]