ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(271) * Warning 271 at /__w/FStar/FStar/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

(271) * Warning 271 at /__w/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 /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(435,8-435,51)

(271) * Warning 271 at /__w/FStar/FStar/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

(288) * Warning 288 at /__w/FStar/FStar/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(448,0-448,42)

(271) * Warning 271 at /__w/FStar/FStar/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/FStar/FStar/FStar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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/data/FStarC.RBSet.fst(105,36-105,37): - 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(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(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 '@'.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(271) * Warning 271 at /__w/FStar/FStar/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

(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(1224,66-1224,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(1224,55-1224,56)

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

(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.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(138,4-138,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.FiniteMap.Base.fst(145,4-145,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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(28,4-28,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.fsti(435,8-435,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.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(435,8-435,51)

(271) * Warning 271 at /home/runner/work/FStar/FStar/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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,36-105,37): - 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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Plugins.fst(89,16-89,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 '@'.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(28,4-28,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.fsti(435,8-435,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.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(435,8-435,51)

(271) * Warning 271 at /home/runner/work/FStar/FStar/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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,36-105,37): - 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 '@'.

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

(337) * Warning 337 at /home/runner/work/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 /home/runner/work/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 /home/runner/work/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 '@'.

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst(28,4-28,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.fsti(435,8-435,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.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(435,8-435,51)

(271) * Warning 271 at /home/runner/work/FStar/FStar/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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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 /home/runner/work/FStar/FStar/fstar/src/data/FStarC.RBSet.fst(105,36-105,37): - 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 '@'.

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

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

(337) * Warning 337 at /home/runner/work/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 /home/runner/work/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 '@'.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

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

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.Free.fst(132,4-134,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.Free.fst(133,4-134,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.FreeFunExt.fst(136,4-138,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.FreeFunExt.fst(137,4-138,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.Par.fst(40,18-40,40): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.Par.fst(48,18-48,40): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.Par.fst(105,4-106,17): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at /__w/FStar/FStar/doc/book/code/Part2.ST.fst(26,2-28,10): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

time = 0.13

time = 0.14

time = 0.18

time = 0.22

time = 0.30

time = 0.47