(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

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(298,15-298,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(298,15-298,17)) and t1 (bound in Pulse.Syntax.Base.fst(172,20-172,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/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.

(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

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(90,4-90,9): - Parameter 0 of items is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(83,4-83,10): - Parameter 0 of values is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(151,4-151,12): - Parameter 0 of disjoint is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(144,4-144,9): - Parameter 0 of equal is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(137,4-137,10): - Parameter 0 of subset is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(151,4-151,12): - Parameter 0 of disjoint is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(144,4-144,9): - Parameter 0 of equal is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(137,4-137,10): - Parameter 0 of subset is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.Monotonic.Witnessed.fsti(34,4-34,33): - Expected parameter 'state of witnessed to be unused in its definition and eliminated - See also /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(55,0-55,56)

(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,66-642,67): - Inserted an unsafe type coercion in generated code from unit -> 'a -> 'a to unit -> 'a -> 'b. - This may be unsound in F#. - See also /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,55-642,56)

(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(247,42-247,60): - Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE 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 /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) 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 /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) 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

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33): - 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/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33): - 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/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GhostSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction - See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(436,8-436,51)

(271) * Warning 271 at /home/runner/work/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

(271) * Warning 271 at /home/runner/work/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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(26,4-26,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(247,42-247,60): - Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE 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 /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) 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 /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) 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

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33): - 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/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(126,12-126,15)

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(122,0-131,33): - 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/FStar/FStar/fstar/ulib/FStar.WellFounded.fst(86,12-86,15)

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GhostSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst(293,8-293,25): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction - See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti(436,8-436,51)

(271) * Warning 271 at /home/runner/work/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

(271) * Warning 271 at /home/runner/work/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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(26,4-26,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(274) * Warning 274: - Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses' in file "Typeclasses.fst". - Rename "Typeclasses.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file "Pure.fst". - Rename "Pure.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

(361) * Warning 361 at AlexOpaque.fst(103,0-125,5): - Some #push-options have not been popped. Current depth is 2.

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

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

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

(274) * Warning 274: - Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses' in file "Typeclasses.fst". - Rename "Typeclasses.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file "Pure.fst". - Rename "Pure.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

time = 1.06

time = 0.57

time = 0.34

time = 0.23

time = 0.17

time = 0.15