Process completed with exit code 2.

(12) * Error 12 at PulseTutorial.Array.fst(201,2-201,26): - Ill-typed term: Seq.Base.lemma_eq_elim s1 's2 - Expected type FStar.Seq.Base.seq (*?u1279*)_ but s1 has type FStar.SizeT.t

(76) * Error 76 at PulseTutorial.Array.fst(201,2-201,19): - Ill-typed term: Seq.Base.lemma_eq_elim s1 's2 - tc_term callback failed: Top () > top (FStar.Seq.Base.lemma_eq_elim s1 's2) >> app subtyping (s1) >>> check_subtype (FStar.SizeT.t ( <:? s1) FStar.Seq.Base.seq t) - (not equatable) FStar.SizeT.t is not a subtype of FStar.Seq.Base.seq t

(228) * Error 228 at PulseTutorial.LinkedList.fst(281,2-281,22): - Tactic failed - Cannot prove: is_list ll (*?u1209*)_ - In the context: trade (is_list _sfx __suffix1213) (is_list x 'l) is_list _sfx __suffix1213 Pulse.Lib.Reference.pts_to ctr ll Pulse.Lib.Reference.pts_to cur _sfx

(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(299,14-299,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(299,14-299,16)) and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,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/pulse/pulse/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/pulse/pulse/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/pulse/pulse/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/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(957,4-957,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/pulse/pulse/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/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(663,47-663,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/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(662,47-662,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/pulse/pulse/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