Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.output and /tests/error-messages/AQualMismatch.fst.output.expected: --- _output/AQualMismatch.fst.output 2025-03-04 22:58:31.985071164 +0000 +++ AQualMismatch.fst.output.expected 2025-03-04 22:56:02.848798902 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at AQualMismatch.fst:6.7-6.8: +* Error 91 at AQualMismatch.fst(6,7-6,8): - Inconsistent implicit argument annotation on argument x - Got: '#' - Expected: '' >>] -* Warning 240 at AQualMismatch.fst:3.4-3.5: +* Warning 240 at AQualMismatch.fst(3,4-3,5): - AQualMismatch.f is declared but no definition was found - Add an 'assume' if this is intentional -* Warning 240 at AQualMismatch.fst:6.0-6.12: +* Warning 240 at AQualMismatch.fst(6,0-6,12): - Missing definitions in module AQualMismatch: f

Diff failed for files /tests/error-messages/_output/AnotType.fst.output and /tests/error-messages/AnotType.fst.output.expected: --- _output/AnotType.fst.output 2025-03-04 22:58:32.380074220 +0000 +++ AnotType.fst.output.expected 2025-03-04 22:56:02.848798902 +0000 @@ -1,11 +1,11 @@ >> Got issues: [ -* Error 309 at AnotType.fst:19.5-19.7: +* Error 309 at AnotType.fst(19,5-19,7): - Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers >>] >> Got issues: [ -* Error 189 at AnotType.fst:27.14-27.16: +* Error 189 at AnotType.fst(27,14-27,16): - Expected expression of type Type0 got expression tb of type Type >>]

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.output and /tests/error-messages/ArgsAndQuals.fst.output.expected: --- _output/ArgsAndQuals.fst.output 2025-03-04 22:58:32.729076920 +0000 +++ ArgsAndQuals.fst.output.expected 2025-03-04 22:56:02.848798902 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at ArgsAndQuals.fst:25.16-25.18: +* Error 91 at ArgsAndQuals.fst(25,16-25,18): - Inconsistent implicit argument annotation on argument uu___ - Got: '#' - Expected: '$' >>] -* Warning 240 at ArgsAndQuals.fst:23.4-23.9: +* Warning 240 at ArgsAndQuals.fst(23,4-23,9): - ArgsAndQuals.test1 is declared but no definition was found - Add an 'assume' if this is intentional -* Warning 240 at ArgsAndQuals.fst:25.0-25.29: +* Warning 240 at ArgsAndQuals.fst(25,0-25,29): - Missing definitions in module ArgsAndQuals: test1

Diff failed for files /tests/error-messages/_output/ArgsMismatch.fst.output and /tests/error-messages/ArgsMismatch.fst.output.expected: --- _output/ArgsMismatch.fst.output 2025-03-04 22:58:33.092079728 +0000 +++ ArgsMismatch.fst.output.expected 2025-03-04 22:56:02.848798902 +0000 @@ -1,78 +1,78 @@ >> Got issues: [ -* Error 173 at ArgsMismatch.fst:7.33-7.34: +* Error 173 at ArgsMismatch.fst(7,33-7,34): - Too many arguments to function of type y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 92 at ArgsMismatch.fst:8.35-8.36: +* Error 92 at ArgsMismatch.fst(8,35-8,36): - Inconsistent argument qualifiers. - Expected an implicit argument, got an explicit one. >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:10.34-10.35: +* Error 173 at ArgsMismatch.fst(10,34-10,35): - Too many arguments to function of type y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:14.33-14.34: +* Error 173 at ArgsMismatch.fst(14,33-14,34): - Too many arguments to function of type y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 92 at ArgsMismatch.fst:15.35-15.36: +* Error 92 at ArgsMismatch.fst(15,35-15,36): - Inconsistent argument qualifiers. - Expected an implicit argument, got an explicit one. >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:17.34-17.35: +* Error 173 at ArgsMismatch.fst(17,34-17,35): - Too many arguments to function of type y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:21.33-21.34: +* Error 173 at ArgsMismatch.fst(21,33-21,34): - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 92 at ArgsMismatch.fst:22.35-22.36: +* Error 92 at ArgsMismatch.fst(22,35-22,36): - Inconsistent argument qualifiers. - Expected an implicit argument, got an explicit one. >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:24.34-24.35: +* Error 173 at ArgsMismatch.fst(24,34-24,35): - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:28.33-28.34: +* Error 173 at ArgsMismatch.fst(28,33-28,34): - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int >>] >> Got issues: [ -* Error 92 at ArgsMismatch.fst:29.35-29.36: +* Error 92 at ArgsMismatch.fst(29,35-29,36): - Inconsistent argument qualifiers. - Expected an implicit argument, got an explicit one. >>] >> Got issues: [ -* Error 173 at ArgsMismatch.fst:31.34-31.35: +* Error 173 at ArgsMismatch.fst(31,34-31,35): - Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int - Got 2 arguments - Remaining type is Prims.int

Diff failed for files /tests/error-messages/_output/ArrowRanges.fst.output and /tests/error-messages/ArrowRanges.fst.output.expected: --- _output/ArrowRanges.fst.output 2025-03-04 22:58:33.616083783 +0000 +++ ArrowRanges.fst.output.expected 2025-03-04 22:56:02.848798902 +0000 @@ -1,20 +1,20 @@ >> Got issues: [ -* Error 19 at ArrowRanges.fst:4.30-4.39: +* Error 19 at ArrowRanges.fst(4,30-4,39): - Subtyping check failed - Expected type Prims.eqtype got type Type0 - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst:81.23-81.30 + - See also Prims.fst(81,23-81,30) >>] >> Got issues: [ -* Error 19 at ArrowRanges.fst:8.10-8.28: +* Error 19 at ArrowRanges.fst(8,10-8,28): - Failed to prove that the type 'ArrowRanges.ppof' supports decidable equality because of this argument. - Add either the 'noeq' or 'unopteq' qualifier - The SMT solver could not prove the query. Use --query_stats for more details. - - See also ArrowRanges.fst:7.0-11.1 + - See also ArrowRanges.fst(7,0-11,1) >>]

Diff failed for files /tests/error-messages/_output/AssertNorm.fst.output and /tests/error-messages/AssertNorm.fst.output.expected: --- _output/AssertNorm.fst.output 2025-03-04 22:58:34.036087115 +0000 +++ AssertNorm.fst.output.expected 2025-03-04 22:56:02.849798911 +0000 @@ -1,8 +1,8 @@ >> Got issues: [ -* Error 19 at AssertNorm.fst:7.2-7.13: +* Error 19 at AssertNorm.fst(7,2-7,13): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also AssertNorm.fst:7.14-7.30 + - See also AssertNorm.fst(7,14-7,30) >>]

Diff failed for files /tests/error-messages/_output/Asserts.fst.output and /tests/error-messages/Asserts.fst.output.expected: --- _output/Asserts.fst.output 2025-03-04 22:58:34.533091201 +0000 +++ Asserts.fst.output.expected 2025-03-04 22:56:02.849798911 +0000 @@ -1,23 +1,23 @@ >> Got issues: [ -* Error 19 at Asserts.fst:6.9-6.17: +* Error 19 at Asserts.fst(6,9-6,17): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. >>] >> Got issues: [ -* Error 19 at Asserts.fst:11.2-11.8: +* Error 19 at Asserts.fst(11,2-11,8): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Asserts.fst:11.9-11.17 + - See also Asserts.fst(11,9-11,17) >>] >> Got issues: [ -* Error 19 at Asserts.fst:16.2-16.8: +* Error 19 at Asserts.fst(16,2-16,8): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Asserts.fst:16.9-16.14 + - See also Asserts.fst(16,9-16,14) >>]

Diff failed for files /tests/error-messages/_output/BadEmptyRecord.fst.output and /tests/error-messages/BadEmptyRecord.fst.output.expected: --- _output/BadEmptyRecord.fst.output 2025-03-04 22:58:34.885094096 +0000 +++ BadEmptyRecord.fst.output.expected 2025-03-04 22:56:02.849798911 +0000 @@ -1,5 +1,5 @@ >> Got issues: [ -* Error 360 at BadEmptyRecord.fst:9.6-9.8: +* Error 360 at BadEmptyRecord.fst(9,6-9,8): - Could not resolve the type for this record. >>]

Diff failed for files /tests/error-messages/_output/Basic.fst.output and /tests/error-messages/Basic.fst.output.expected: --- _output/Basic.fst.output 2025-03-04 22:58:35.480098968 +0000 +++ Basic.fst.output.expected 2025-03-04 22:56:02.849798911 +0000 @@ -1,93 +1,93 @@ >> Got issues: [ -* Error 189 at Basic.fst:4.13-4.17: +* Error 189 at Basic.fst(4,13-4,17): - Expected expression of type Prims.int got expression true of type Prims.bool >>] >> Got issues: [ -* Error 19 at Basic.fst:6.38-6.44: +* Error 19 at Basic.fst(6,38-6,44): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:6.45-6.50 + - See also Basic.fst(6,45-6,50) >>] >> Got issues: [ -* Error 19 at Basic.fst:7.38-7.44: +* Error 19 at Basic.fst(7,38-7,44): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:7.45-7.50 + - See also Basic.fst(7,45-7,50) >>] >> Got issues: [ -* Error 19 at Basic.fst:8.38-8.44: +* Error 19 at Basic.fst(8,38-8,44): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:8.45-8.50 + - See also Basic.fst(8,45-8,50) >>] >> Got issues: [ -* Error 19 at Basic.fst:9.38-9.44: +* Error 19 at Basic.fst(9,38-9,44): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:9.45-9.50 + - See also Basic.fst(9,45-9,50) >>] >> Got issues: [ -* Error 19 at Basic.fst:11.38-11.49: +* Error 19 at Basic.fst(11,38-11,49): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:11.50-11.55 + - See also Basic.fst(11,50-11,55) >>] >> Got issues: [ -* Error 19 at Basic.fst:12.38-12.49: +* Error 19 at Basic.fst(12,38-12,49): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:12.50-12.55 + - See also Basic.fst(12,50-12,55) >>] >> Got issues: [ -* Error 19 at Basic.fst:13.38-13.49: +* Error 19 at Basic.fst(13,38-13,49): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:13.50-13.55 + - See also Basic.fst(13,50-13,55) >>] >> Got issues: [ -* Error 19 at Basic.fst:14.38-14.49: +* Error 19 at Basic.fst(14,38-14,49): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Basic.fst:14.50-14.55 + - See also Basic.fst(14,50-14,55) >>] >> Got issues: [ -* Error 19 at Basic.fst:17.29-17.31: +* Error 19 at Basic.fst(17,29-17,31): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst:459.90-459.102 + - See also Prims.fst(459,90-459,102) >>] >> Got issues: [ -* Error 19 at Basic.fst:20.29-20.31: +* Error 19 at Basic.fst(20,29-20,31): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst:459.90-459.102 + - See also Prims.fst(459,90-459,102) >>] >> Got issues: [ -* Error 19 at Basic.fst:23.46-23.48: +* Error 19 at Basic.fst(23,46-23,48): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Prims.fst:459.90-459.102 + - See also Prims.fst(459,90-459,102) >>]

Diff failed for files /tests/error-messages/_output/Bug1918.fst.output and /tests/error-messages/Bug1918.fst.output.expected: --- _output/Bug1918.fst.output 2025-03-04 22:58:36.379106329 +0000 +++ Bug1918.fst.output.expected 2025-03-04 22:56:02.849798911 +0000 @@ -1,6 +1,6 @@ >> Got issues: [ -* Error 228 at Bug1918.fst:11.13-11.14: +* Error 228 at Bug1918.fst(11,13-11,14): - Could not solve typeclass constraint `Bug1918.mon` - - See also FStar.Tactics.Typeclasses.fst:293.6-296.7 + - See also FStar.Tactics.Typeclasses.fst(293,6-296,7) >>]

Process completed with exit code 1.

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

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

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

(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(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(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(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

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

(345) * Warning 345: - Inserted an unsafe type coercion in generated code from some_ref -> (obj, obj) mreference to some_ref -> (unit, unit) mreference. - This may be unsound in F#.

(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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:27.4-27.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

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

(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

(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

(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

(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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GSet.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.

The Ubuntu-20.04 brownout takes place from 2025-02-01. For more details, see https://github.com/actions/runner-images/issues/11101

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:27.4-27.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

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

(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

(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

(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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GSet.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.

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:27.4-27.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

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

(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

(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

(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

(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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.GSet.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.

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

(350) * Warning 350 at 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 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 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 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 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 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 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 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.

(350) * Warning 350 at Part2.ST.fst:27.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.

time = 0.10

time = 0.12

time = 0.14

time = 0.18

time = 0.29

time = 0.45