Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.json_output and /tests/error-messages/AQualMismatch.fst.json_output.expected: --- _output/AQualMismatch.fst.json_output 2025-01-17 06:22:35.889801682 +0000 +++ AQualMismatch.fst.json_output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,5 +1,5 @@ >> Got issues: [ -{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":8},"end_pos":{"line":6,"col":9}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":8},"end_pos":{"line":6,"col":9}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +{"msg":["Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Error","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":7},"end_pos":{"line":6,"col":8}}},"number":91,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} >>] -{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":5},"end_pos":{"line":3,"col":6}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":5},"end_pos":{"line":3,"col":6}}},"number":240,"ctx":["While desugaring module AQualMismatch"]} -{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}}},"number":240,"ctx":[]} +{"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]} +{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}

Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.output and /tests/error-messages/AQualMismatch.fst.output.expected: --- _output/AQualMismatch.fst.output 2025-01-17 06:22:36.075802491 +0000 +++ AQualMismatch.fst.output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at AQualMismatch.fst:6.8-6.9: +* Error 91 at AQualMismatch.fst(6,7-6,8): - Inconsistent implicit argument annotation on argument x - Got: '#' - Expected: '' >>] -* Warning 240 at AQualMismatch.fst:3.5-3.6: +* 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.1-6.13: +* 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.json_output and /tests/error-messages/AnotType.fst.json_output.expected: --- _output/AnotType.fst.json_output 2025-01-17 06:22:36.267803326 +0000 +++ AnotType.fst.json_output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,6 +1,6 @@ >> Got issues: [ -{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":6},"end_pos":{"line":19,"col":8}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":6},"end_pos":{"line":19,"col":8}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]} +{"msg":["Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}},"use":{"file_name":"AnotType.fst","start_pos":{"line":19,"col":5},"end_pos":{"line":19,"col":7}}},"number":309,"ctx":["While typechecking the top-level declaration `type AnotType.tc`","While typechecking the top-level declaration `[@@expect_failure] type AnotType.tc`"]} >>] >> Got issues: [ -{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":15},"end_pos":{"line":27,"col":17}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":15},"end_pos":{"line":27,"col":17}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} +{"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} >>]

Diff failed for files /tests/error-messages/_output/AnotType.fst.output and /tests/error-messages/AnotType.fst.output.expected: --- _output/AnotType.fst.output 2025-01-17 06:22:36.515804405 +0000 +++ AnotType.fst.output.expected 2025-01-17 06:20:14.466184877 +0000 @@ -1,11 +1,11 @@ >> Got issues: [ -* Error 309 at AnotType.fst:19.6-19.8: +* 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.15-27.17: +* 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.json_output and /tests/error-messages/ArgsAndQuals.fst.json_output.expected: --- _output/ArgsAndQuals.fst.json_output 2025-01-17 06:22:36.741805387 +0000 +++ ArgsAndQuals.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,5 +1,5 @@ >> Got issues: [ -{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":17},"end_pos":{"line":25,"col":19}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":17},"end_pos":{"line":25,"col":19}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} +{"msg":["Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Error","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":16},"end_pos":{"line":25,"col":18}}},"number":91,"ctx":["While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} >>] -{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":5},"end_pos":{"line":23,"col":10}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":5},"end_pos":{"line":23,"col":10}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]} -{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}}},"number":240,"ctx":[]} +{"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]} +{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.output and /tests/error-messages/ArgsAndQuals.fst.output.expected: --- _output/ArgsAndQuals.fst.output 2025-01-17 06:22:36.916806148 +0000 +++ ArgsAndQuals.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,14 +1,14 @@ >> Got issues: [ -* Error 91 at ArgsAndQuals.fst:25.17-25.19: +* Error 91 at ArgsAndQuals.fst(25,16-25,18): - Inconsistent implicit argument annotation on argument uu___ - Got: '#' - Expected: '$' >>] -* Warning 240 at ArgsAndQuals.fst:23.5-23.10: +* 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.1-25.30: +* Warning 240 at ArgsAndQuals.fst(25,0-25,29): - Missing definitions in module ArgsAndQuals: test1

Diff failed for files /tests/error-messages/_output/ArrowRanges.fst.json_output and /tests/error-messages/ArrowRanges.fst.json_output.expected: --- _output/ArrowRanges.fst.json_output 2025-01-17 06:22:37.182807305 +0000 +++ ArrowRanges.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,6 +1,6 @@ >> Got issues: [ -{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":24},"end_pos":{"line":73,"col":31}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":31},"end_pos":{"line":4,"col":40}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]} +{"msg":["Subtyping check failed","Expected type Prims.eqtype\ngot type Type0","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":73,"col":23},"end_pos":{"line":73,"col":30}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":4,"col":30},"end_pos":{"line":4,"col":39}}},"number":19,"ctx":["While typechecking the top-level declaration `let ppof`","While typechecking the top-level declaration `[@@expect_failure] let ppof`"]} >>] >> Got issues: [ -{"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports 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."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":1},"end_pos":{"line":11,"col":2}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":11},"end_pos":{"line":8,"col":29}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]} +{"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports 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."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":0},"end_pos":{"line":11,"col":1}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":10},"end_pos":{"line":8,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]} >>]

Diff failed for files /tests/error-messages/_output/ArrowRanges.fst.output and /tests/error-messages/ArrowRanges.fst.output.expected: --- _output/ArrowRanges.fst.output 2025-01-17 06:22:37.452808479 +0000 +++ ArrowRanges.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,20 +1,20 @@ >> Got issues: [ -* Error 19 at ArrowRanges.fst:4.31-4.40: +* 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:73.24-73.31 + - See also Prims.fst(73,23-73,30) >>] >> Got issues: [ -* Error 19 at ArrowRanges.fst:8.11-8.29: +* 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.1-11.2 + - See also ArrowRanges.fst(7,0-11,1) >>]

Diff failed for files /tests/error-messages/_output/AssertNorm.fst.json_output and /tests/error-messages/AssertNorm.fst.json_output.expected: --- _output/AssertNorm.fst.json_output 2025-01-17 06:22:37.673809440 +0000 +++ AssertNorm.fst.json_output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,3 +1,3 @@ >> Got issues: [ -{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":15},"end_pos":{"line":7,"col":31}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":3},"end_pos":{"line":7,"col":14}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} +{"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":14},"end_pos":{"line":7,"col":30}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":2},"end_pos":{"line":7,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]} >>]

Diff failed for files /tests/error-messages/_output/AssertNorm.fst.output and /tests/error-messages/AssertNorm.fst.output.expected: --- _output/AssertNorm.fst.output 2025-01-17 06:22:37.887810371 +0000 +++ AssertNorm.fst.output.expected 2025-01-17 06:20:14.467184882 +0000 @@ -1,8 +1,8 @@ >> Got issues: [ -* Error 19 at AssertNorm.fst:7.3-7.14: +* 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.15-7.31 + - See also AssertNorm.fst(7,14-7,30) >>]

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.9-435.52: - 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.9-293.26: - 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.9-435.52

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52: - 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.21-116.32: - 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:446.1-446.43

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti:435.9-435.52: - 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.31-105.32: - 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.37-105.38: - 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.17-86.18: - 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.17-87.18: - 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.17-88.18: - 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

(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti:1224.67-1224.68: - 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.56-1224.57

(344) * Warning 344 at ulib/FStar.FiniteSet.Base.fst:137.5-137.11: - 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 ulib/FStar.FiniteSet.Base.fst:144.5-144.10: - 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 ulib/FStar.FiniteSet.Base.fst:151.5-151.13: - 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.5-34.34: - Expected parameter 'state of witnessed to be unused in its definition and eliminated - See also ulib/FStar.Pervasives.fsti:55.1-55.57

(344) * Warning 344 at ulib/FStar.FiniteMap.Base.fst:83.5-83.11: - 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 ulib/FStar.FiniteMap.Base.fst:90.5-90.10: - 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 ulib/FStar.FiniteMap.Base.fst:138.5-138.10: - 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 ulib/FStar.FiniteMap.Base.fst:145.5-145.13: - 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#.

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.5-28.8: - 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 ulib/FStar.GhostSet.fst:23.5-23.8: - 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 ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:86.13-86.16

(242) * Warning 242 at ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:126.13-126.16

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.9-435.52: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(330) * Warning 330 at ulib/experimental/FStar.MST.fst:222.44-222.56: - 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 ulib/experimental/FStar.MST.fst:247.43-247.61: - 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

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst:293.9-293.26: - 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.9-435.52

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.9-435.52: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(318) * Warning 318 at ulib/FStar.GSet.fst:23.5-23.8: - 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:28.5-28.8: - 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 ulib/FStar.GhostSet.fst:23.5-23.8: - 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 ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:86.13-86.16

(242) * Warning 242 at ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:126.13-126.16

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.1-194.60: - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.LexicographicOrdering.fst:75.15-75.29

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.1-194.60: - Definitions of inner let-rec get_acc and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.LexicographicOrdering.fst:124.11-124.18

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.9-435.52: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(330) * Warning 330 at ulib/experimental/FStar.MST.fst:222.44-222.56: - 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 ulib/experimental/FStar.MST.fst:247.43-247.61: - 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 ulib/FStar.GSet.fst:23.5-23.8: - 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:28.5-28.8: - 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.9-435.52: - 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.9-293.26: - 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.9-435.52

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.9-435.52: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(318) * Warning 318 at ulib/FStar.GhostSet.fst:23.5-23.8: - 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 ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:86.13-86.16

(242) * Warning 242 at ulib/FStar.WellFounded.fst:122.1-131.34: - 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: ulib/FStar.WellFounded.fst:126.13-126.16

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.1-194.60: - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.LexicographicOrdering.fst:75.15-75.29

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.1-194.60: - Definitions of inner let-rec get_acc and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: ulib/FStar.LexicographicOrdering.fst:124.11-124.18

(330) * Warning 330 at ulib/experimental/FStar.MST.fst:222.44-222.56: - 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

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 Hello.fst:5.1-5.35: - Top-level let-bindings must be total; this term may have effects

(350) * Warning 350 at Part2.Free.fst:132.5-134.13: - 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.5-134.13: - 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.5-138.13: - 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.5-138.13: - 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.19-40.41: - 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.19-48.41: - 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.5-106.18: - 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.3-28.11: - 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.3-28.11: - 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.13

time = 0.14

time = 0.16

time = 0.21

time = 0.30

time = 0.46