(66) * Error 66 at out.fail.batch/FAILAllBytesCompose.fst(81,6-87,85): - Failed to resolve implicit argument ?57 of type Prims.bool introduced for Instantiating implicit argument

(12) * Error 12 at out.fail.batch/FAILAllBytesCompose.fst(83,10-85,52): - Expected type EverParse3d.Interpreter.typ (*?u58*) _ (*?u59*) _ (*?u60*) _ (*?u61*) _ (*?u62*) _ (*?u63*) _ but EverParse3d.Interpreter.T_with_comment "should_not_be_here" (EverParse3d.Interpreter.T_denoted "should_not_be_here" dtyp__test1) "Validating field should_not_be_here" has type EverParse3d.Interpreter.typ kind__test1 EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial EverParse3d.Interpreter.Trivial false false

(19) * Error 19 at out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16): - Could not prove goal #1 - The SMT solver could not prove the query. Use --query_stats for more details. - Also see: out.fail.batch/FAILAllBytesNotLast.fst(14,2-34,16) - Other related locations: /__w/everparse/everparse/FStar/stage2/out/lib/fstar/ulib/Prims.fst(467,77-467,89) - See also out.fail.batch/FAILAllBytesNotLast.fst(33,4-34,15)

(189) * Error 189 at out.fail.batch/FAILAllBytesNotLast.fst(43,53-43,67): - Expected expression of type EverParse3d.Kinds.parser_kind (*?u58*) _ EverParse3d.Kinds.WeakKindStrongPrefix got expression EverParse3d.Kinds.kind_all_bytes of type EverParse3d.Kinds.parser_kind false EverParse3d.Kinds.WeakKindConsumesAll

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

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

(337) * Warning 337 at /__w/everparse/everparse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(640,47-640,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/everparse/everparse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(641,47-641,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/everparse/everparse/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 '@'.

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

(290) * Warning 290 at /__w/everparse/everparse/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/everparse/everparse/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.

(290) * Warning 290 at /__w/everparse/everparse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17)) and t1 (bound in Pulse.Syntax.Base.fst(171,20-171,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - 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/everparse/everparse/pulse/src/checker/Pulse.Syntax.Base.fst(293,15-293,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst(293,15-293,17)) and q1 (bound in Pulse.Syntax.Base.fst(298,14-298,16)) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: Pulse.Syntax.Base.qualifier - If the proof fails, try annotating these with the same type.

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

(337) * Warning 337 at /__w/everparse/everparse/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 '@'.

(337) * Warning 337 at /__w/everparse/everparse/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/everparse/everparse/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/everparse/everparse/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 '@'.

(328) * Warning 328 at /__w/everparse/everparse/FStar/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body

(328) * Warning 328 at /__w/everparse/everparse/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

(328) * Warning 328 at /__w/everparse/everparse/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/everparse/everparse/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/everparse/everparse/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(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

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

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

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

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

(361) * Warning 361 at LowParse.Spec.BoundedInt.fsti(232,0-235,62): - Some #push-options have not been popped. Current depth is 1.

(271) * Warning 271 at LowParse.Spec.Base.fsti(544,13-546,17): - Pattern misses at least one bound variable: t

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

(361) * Warning 361 at LowParse.BitFields.fst(1276,0-1276,29): - Some #push-options have not been popped. Current depth is 1.

(337) * Warning 337 at LowParse.Low.Base.Spec.fst(487,8-487,18): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(328) * Warning 328 at LowParse.Low.Base.Spec.fst(511,8-511,24): - Global binding 'LowParse.Low.Base.Spec.valid_list_equiv' is recursive but not used in its body

(337) * Warning 337 at LowParse.Low.Base.Spec.fst(548,8-548,21): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(337) * Warning 337 at LowParse.Low.Base.Spec.fst(612,8-612,41): - This definitions has multiple decreases clauses. - The decreases clause on the declaration is ignored, please remove it.

(328) * Warning 328 at LowParse.Spec.Enum.fst(107,8-107,24): - Global binding 'LowParse.Spec.Enum.assoc_flip_intro' is recursive but not used in its body