(361) * Warning 361 at /home/runner/.hax/hacl_home/lib/Lib.IntTypes.fsti(988,0-988,21): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at /home/runner/.hax/hacl_home/lib/Lib.Sequence.fsti(599,0-613,142): - Some #push-options have not been popped. Current depth is 1.

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(74,0-80,10): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(328,0-328,12): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/Tactics.Utils.fst(75,12-75,15)

(242) * Warning 242 at /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(223,0-229,12): - Definitions of inner let-rec h and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/libcrux/libcrux/fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti(225,12-225,13)