Process completed with exit code 1.

Process completed with exit code 1.

Process completed with exit code 1.

Process completed with exit code 2.

(19) * Error 19 at src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Serialized.Base.fst(153,14-153,28): - Ill-typed term: CBOR.Spec.Raw.EverParse.get_tagged_tag v h - Assertion failed - Also see: src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.EverParse.Serialized.Base.fst(153,14-153,28) - Other related locations: src/cbor/spec/raw/everparse/CBOR.Spec.Raw.EverParse.fst(1383,57-1383,66)

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1989,4-1989,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(1725,4-1725,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(1093,4-1093,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(754,4-754,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(733,8-733,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

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

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

(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 (["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", "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(304,14-304,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(304,14-304,16)) and t1 (bound in Pulse.Syntax.Base.fst(171,20-171,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(892,4-892,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(635,47-635,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(634,47-634,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(526,8-526,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(376,8-376,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.

(249) * Warning 249 at Bug166.fst(13,9-13,10): - Losing precision when encoding a function literal: fun _ -> Pulse.Lib.Core.emp - Unannotated abstraction in the compiler? - See also Bug166.fst(9,11-9,14)

(249) * Warning 249 at Bug166.fst(13,9-13,10): - Losing precision when encoding a function literal: fun _ -> Pulse.Lib.Core.emp - Unannotated abstraction in the compiler? - See also Bug166.fst(9,11-9,14)

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

(361) * Warning 361 at PulseTutorial.Array.fst(269,0-278,1): - Some #push-options have not been popped. Current depth is 1.

(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.

(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 '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 "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 "/__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.

(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

(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