(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1991,4-1991,12): - Global binding 'FStarC.Parser.ToDocument.p_tmNoEq' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1727,4-1727,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(436,8-436,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,34-58,41): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,11-58,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also FStar.Krml.Endianness.fst(36,4-36,28)

(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(328) * Warning 328 at Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body

* Warning <unknown> at Examples.Guess.fst(87,5-87,20): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(109,85-109,111)

* Warning <unknown> at Examples.Guess.fst(87,5-87,20): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(109,42-109,68)

* Warning <unknown> at Examples.Guess.fst(79,2-79,17): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(361,83-361,107)

(272) * Warning 272 at Monitor.fst(15,0-15,36): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at GoodHandler1.fst(150,0-150,37): - Some #push-options have not been popped. Current depth is 1.

(272) * Warning 272 at GoodHandler1.fst(150,0-150,37): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at StlcHandlers.fst(121,0-124,16): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at ../../Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at WebServer.fst(237,0-238,38): - Some #push-options have not been popped. Current depth is 1.

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(390,8-390,42)

(349) * Warning 349 at Utils.fst(377,2-381,5): - The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.

(352) * Warning 352 at ../../MIO.fst(217,27-217,44): - Combinator Prims.PURE ~> MIO.MIOwp is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(242) * Warning 242 at case-studies/IOLogging.fst(111,0-118,59): - 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: case-studies/IOLogging.fst(112,11-112,14)

* Warning <unknown> at case-studies/IOLogging.fst(103,3-103,33): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at case-studies/Compiler.Model1.Examples.fst(202,22-202,52): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(390,8-390,42)

* Warning <unknown> at case-studies/NoState.fst(75,57-75,62): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

* Warning <unknown> at case-studies/Zip.fst(59,76-59,81): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(136,0-143,58): - 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: case-studies/Compiler.Model1.Examples.fst(137,10-137,13)

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(95,0-103,58): - 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: case-studies/Compiler.Model1.Examples.fst(96,10-96,13)

(242) * Warning 242 at case-studies/NoState.fst(48,0-56,58): - 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: case-studies/NoState.fst(49,10-49,13)

(361) * Warning 361 at Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.

(352) * Warning 352 at MIO.fst(217,27-217,44): - Combinator Prims.PURE ~> MIO.MIOwp is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(242) * Warning 242: - Not extracting uu___is_S to KaRaMeL

(272) * Warning 272 at Wasm10.fst(16,0-17,77): - Top-level let-bindings must be total; this term may have effects

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting (["FStar", "Tactics", "NamedView"], "close_term_n") to KaRaMeL. - Got an exception:Failure("Internal error: name not found aux\n")

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(285) * Warning 285 at TopLevelArray.fst(7,5-7,7): - No modules in namespace ST and no file with that name either

(285) * Warning 285 at MemCpyModel.fst(10,5-10,7): - No modules in namespace ST and no file with that name either

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti(185,16-185,20): - Combinator (Steel.ST.Effect.AtomicAndGhost.STAGCommon , Steel.ST.Effect.AtomicAndGhost.STAGCommon) |> Steel.ST.Effect.AtomicAndGhost.STAGCommon is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(340) * Warning 340 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(461,24-461,37): - Unfolding name which is marked as a plugin: frame_vc_norm - See also /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(415,4-415,17)

(337) * Warning 337 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2066,65-2066,66): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(303,14-303,16): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of q1 (bound in Pulse.Syntax.Base.fst(303,14-303,16)) and t1 (bound in Pulse.Syntax.Base.fst(172,20-172,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.qualifier - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(123,20-123,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) and pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(139,16-139,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) and p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool - The type of the second term is: Pulse.Syntax.Base.pattern - If the proof fails, try annotating these with the same type.

(318) * Warning 318 at /__w/FStar/FStar/pulse/lib/common/Pulse.Lib.Raise.fst(21,4-21,12): - Values of type `raisable` will be erased during extraction, but its interface hides this fact. - Add the `must_erase_for_extraction` attribute to the `val raisable` declaration for this symbol in the interface

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(926,4-926,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/checker/Pulse.Common.fst(84,11-84,12): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(659,47-659,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(658,47-658,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(545,8-545,17): - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(397,8-397,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(330) * Warning 330 at SteelT.Effect.fst(51,44-51,59): - Polymonadic binds ((SteelT, PURE) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(51,0-51,59): - Combinator (SteelT.Effect.SteelT , Prims.PURE) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(330) * Warning 330 at SteelT.Effect.fst(51,44-51,59): - Polymonadic binds ((SteelT, PURE) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(51,0-51,59): - Combinator (SteelT.Effect.SteelT , Prims.PURE) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(330) * Warning 330 at SteelT.Effect.fst(41,44-41,59): - Polymonadic binds ((PURE, SteelT) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(330) * Warning 330 at SteelT.Effect.fst(41,44-41,59): - Polymonadic binds ((PURE, SteelT) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(31,9-31,13): - Combinator (SteelT.Effect.SteelT , SteelT.Effect.SteelT) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at SteelT.Effect.fst(31,9-31,13): - Combinator (SteelT.Effect.SteelT , SteelT.Effect.SteelT) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(274) * Warning 274: - Implicitly opening namespace 'duplex.' shadows module 'pingpong' in file "PingPong.fst". - Rename "PingPong.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'cqueue.' shadows module 'llist' in file "LList.fst". - Rename "LList.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'cddl.' shadows module 'pulse' in file "/__w/FStar/FStar/pulse/out/lib/pulse/lib/Pulse.fst". - Rename "/__w/FStar/FStar/pulse/out/lib/pulse/lib/Pulse.fst" to avoid conflicts.

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(136,13-136,14): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(131,21-131,22): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(285) * Warning 285 at PulseTutorial.LinkedList.fst(223,5-223,6): - No modules in namespace I and no file with that name either

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(285) * Warning 285 at PulseTutorial.LinkedList.fst(223,5-223,6): - No modules in namespace I and no file with that name either

(285) * Warning 285 at PulseTutorial.ImplicationAndForall.fst(24,5-24,7): - No modules in namespace GR and no file with that name either

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(272) * Warning 272 at ./src/Prelude.fst(8,0-8,48): - Top-level let-bindings must be total; this term may have effects

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "src/Prelude.fst". - Rename "src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "./src/Prelude.fst". - Rename "./src/Prelude.fst" to avoid conflicts.

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Scalar to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Scalar.fsti.checked instead of _cache/Steel.ST.C.Types.Scalar.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Rewrite to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Rewrite.fsti.checked instead of _cache/Steel.ST.C.Types.Rewrite.fsti.checked

(321) * Warning 321: - Did not expect module Steel.C.Typestring to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typestring.fst.checked instead of _cache/Steel.C.Typestring.fst.checked

(321) * Warning 321: - Did not expect module Steel.C.Typestring to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typestring.fsti.checked instead of _cache/Steel.C.Typestring.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Fields to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Fields.fsti.checked instead of _cache/Steel.ST.C.Types.Fields.fsti.checked

(321) * Warning 321: - Did not expect module Steel.C.Typenat to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typenat.fst.checked instead of _cache/Steel.C.Typenat.fst.checked

(321) * Warning 321: - Did not expect module Steel.C.Typenat to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typenat.fsti.checked instead of _cache/Steel.C.Typenat.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Array to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Array.fsti.checked instead of _cache/Steel.ST.C.Types.Array.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Struct.Aux to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Struct.Aux.fsti.checked instead of _cache/Steel.ST.C.Types.Struct.Aux.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Base to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Base.fsti.checked instead of _cache/Steel.ST.C.Types.Base.fsti.checked

(290) * Warning 290 at Binding.fst(470,22-470,25): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of ts1 (bound in Binding.fst(470,22-470,25)) and t1 (bound in Binding.fst(459,25-459,27)) are equal. - The type of the first term is: Prims.list Ast.typ - The type of the second term is: Ast.typ - If the proof fails, try annotating these with the same type.

(271) * Warning 271 at src/lowparse/LowParse.Spec.Base.fsti(546,14-546,16): - SMT pattern misses at least one bound variable: t

(271) * Warning 271 at src/lowparse/LowParse.Spec.Base.fsti(546,6-546,17): - Pattern misses at least one bound variable: t

(242) * Warning 242 at Ast.fst(1795,0-1797,54): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(418,12-418,15)

(290) * Warning 290 at Ast.fst(1477,16-1477,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in Ast.fst(1477,16-1477,18)) and ts1 (bound in Ast.fst(1491,13-1491,16)) are equal. - The type of the first term is: Ast.typ - The type of the second term is: Prims.list Ast.typ - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at Ast.fst(1491,13-1491,16): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of ts1 (bound in Ast.fst(1491,13-1491,16)) and t1 (bound in Ast.fst(1477,16-1477,18)) are equal. - The type of the first term is: Prims.list Ast.typ - The type of the second term is: Ast.typ - If the proof fails, try annotating these with the same type.

(242) * Warning 242 at Ast.fst(416,0-450,18): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(418,12-418,15)

(361) * Warning 361 at Options.fst(634,0-637,15): - Some #push-options have not been popped. Current depth is 1.

(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/FStar/FStar/karamel/krmllib/C.fst". - Rename "/__w/FStar/FStar/karamel/krmllib/C.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/FStar/FStar/karamel/krmllib/C.fst". - Rename "/__w/FStar/FStar/karamel/krmllib/C.fst" to avoid conflicts.

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExample9.fsti.hints; ran without hints

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExample2.fsti.hints; ran without hints

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExampleConstInt32le.fst.hints; ran without hints

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "igcmalloc_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "ialloca_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21): - Some #push-options have not been popped. Current depth is 1.

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(321) * Warning 321: - Did not expect module FStar.Pervasives to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Pervasives.fsti.checked instead of cache/Model/FStar.Pervasives.fsti.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fst.checked instead of cache/Model/FStar.NormSteps.fst.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fsti.checked instead of cache/Model/FStar.NormSteps.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Attributes to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Attributes.fsti.checked instead of cache/Model/FStar.Attributes.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Prelude to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Prelude.fsti.checked instead of cache/Model/FStar.Prelude.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Mul to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Mul.fst.checked instead of cache/Model/FStar.Mul.fst.checked

(321) * Warning 321: - Did not expect module Prims to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/Prims.fst.checked instead of cache/Model/Prims.fst.checked

(321) * Warning 321: - Did not expect module FStar.UInt32 to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.UInt32.fsti.checked instead of cache/Model/FStar.UInt32.fsti.checked

(321) * Warning 321: - Did not expect module LowStar.Buffer to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Buffer.fst.checked instead of cache/Model/LowStar.Buffer.fst.checked

(321) * Warning 321: - Did not expect module LowStar.Modifies to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Modifies.fst.checked instead of cache/Model/LowStar.Modifies.fst.checked

(321) * Warning 321: - Did not expect module FStar.Pervasives to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Pervasives.fsti.checked instead of cache/Karamel/FStar.Pervasives.fsti.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fst.checked instead of cache/Karamel/FStar.NormSteps.fst.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fsti.checked instead of cache/Karamel/FStar.NormSteps.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Attributes to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Attributes.fsti.checked instead of cache/Karamel/FStar.Attributes.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Prelude to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Prelude.fsti.checked instead of cache/Karamel/FStar.Prelude.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Mul to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Mul.fst.checked instead of cache/Karamel/FStar.Mul.fst.checked

(321) * Warning 321: - Did not expect module Prims to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/Prims.fst.checked instead of cache/Karamel/Prims.fst.checked

(321) * Warning 321: - Did not expect module FStar.UInt32 to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.UInt32.fsti.checked instead of cache/Karamel/FStar.UInt32.fsti.checked

(321) * Warning 321: - Did not expect module LowStar.Buffer to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Buffer.fst.checked instead of cache/Karamel/LowStar.Buffer.fst.checked

(321) * Warning 321: - Did not expect module LowStar.Modifies to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Modifies.fst.checked instead of cache/Karamel/LowStar.Modifies.fst.checked

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "igcmalloc_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "ialloca_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting (["FStar", "Tactics", "NamedView"], "close_term_n") to KaRaMeL. - Got an exception:Failure("Internal error: name not found aux\n")

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Lemmas.fst(300,6-300,7): - Module not found: B

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Lemmas.fst(50,6-50,7): - Module not found: S

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Crypto.fst(70,21-70,23): - Module not found: U8

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Crypto.fst(66,14-66,15): - Module not found: B

(321) * Warning 321: - Did not expect module EverCrypt.CTR.Keys to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/hacl-star/obj/EverCrypt.CTR.Keys.fsti.checked instead of /__w/FStar/FStar/everquic-crypto/obj/EverCrypt.CTR.Keys.fsti.checked

(321) * Warning 321: - Did not expect module EverCrypt.CTR.Keys to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/hacl-star/obj/EverCrypt.CTR.Keys.fst.checked instead of /__w/FStar/FStar/everquic-crypto/obj/EverCrypt.CTR.Keys.fst.checked

(274) * Warning 274: - Implicitly opening namespace 'vale.' shadows module 'lib.meta' in file "/__w/FStar/FStar/hacl-star/lib/Lib.Meta.fst". - Rename "/__w/FStar/FStar/hacl-star/lib/Lib.Meta.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'spec.hash.' shadows module 'test' in file "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst". - Rename "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'model.' shadows module 'quic' in file "src/QUIC.fsti, src/QUIC.fst". - Rename "src/QUIC.fsti, src/QUIC.fst" to avoid conflicts.

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Public.fsti(9,22-9,31): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Public.fsti(4,26-4,30): - module not found in search path: lowparse.spec.base

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fst(7,21-7,30): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fst(5,26-5,37): - module not found in search path: lowparse.spec.combinators

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fsti(12,21-12,30): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.fst(5,21-5,30): - module not found in search path: lowparse.bitfields

(274) * Warning 274: - Implicitly opening namespace 'spec.hash.' shadows module 'test' in file "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst". - Rename "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst" to avoid conflicts.

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Secret.Int.fsti(9,21-9,30): - module not found in search path: lowparse.bitfields

(274) * Warning 274: - Implicitly opening namespace 'model.' shadows module 'quic' in file "src/QUIC.fsti, src/QUIC.fst". - Rename "src/QUIC.fsti, src/QUIC.fst" to avoid conflicts.