Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.output and /tests/error-messages/AQualMismatch.fst.output.expected: --- _output/AQualMismatch.fst.output 2025-02-05 20:40:26.412139315 +0000 +++ AQualMismatch.fst.output.expected 2025-02-05 20:37:56.674222580 +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-02-05 20:40:26.833141877 +0000 +++ AnotType.fst.output.expected 2025-02-05 20:37:56.674222580 +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-02-05 20:40:27.236144330 +0000 +++ ArgsAndQuals.fst.output.expected 2025-02-05 20:37:56.674222580 +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/ArrowRanges.fst.output and /tests/error-messages/ArrowRanges.fst.output.expected: --- _output/ArrowRanges.fst.output 2025-02-05 20:40:27.839147999 +0000 +++ ArrowRanges.fst.output.expected 2025-02-05 20:37:56.674222580 +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:73.23-73.30 + - See also Prims.fst(73,23-73,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-02-05 20:40:28.288150732 +0000 +++ AssertNorm.fst.output.expected 2025-02-05 20:37:56.674222580 +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-02-05 20:40:28.816153975 +0000 +++ Asserts.fst.output.expected 2025-02-05 20:37:56.674222580 +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-02-05 20:40:29.196156312 +0000 +++ BadEmptyRecord.fst.output.expected 2025-02-05 20:37:56.674222580 +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-02-05 20:40:29.799160021 +0000 +++ Basic.fst.output.expected 2025-02-05 20:37:56.674222580 +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:451.90-451.102 + - See also Prims.fst(451,90-451,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:451.90-451.102 + - See also Prims.fst(451,90-451,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:451.90-451.102 + - See also Prims.fst(451,90-451,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-02-05 20:40:30.923166935 +0000 +++ Bug1918.fst.output.expected 2025-02-05 20:37:56.674222580 +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:297.6-300.7 + - See also FStar.Tactics.Typeclasses.fst(297,6-300,7) >>]

Diff failed for files /tests/error-messages/_output/Bug1988.fst.output and /tests/error-messages/Bug1988.fst.output.expected: --- _output/Bug1988.fst.output 2025-02-05 20:40:31.286169167 +0000 +++ Bug1988.fst.output.expected 2025-02-05 20:37:56.675222586 +0000 @@ -1,17 +1,17 @@ >> Got issues: [ -* Error 189 at Bug1988.fst:4.14-4.30: +* Error 189 at Bug1988.fst(4,14-4,30): - Expected expression of type Prims.int got expression "string literal" of type Prims.string >>] >> Got issues: [ -* Error 54 at Bug1988.fst:15.32-15.38: +* Error 54 at Bug1988.fst(15,32-15,38): - Prims.string is not equal to the expected type _: ident -> Prims.string >>] >> Got issues: [ -* Error 54 at Bug1988.fst:21.32-21.38: +* Error 54 at Bug1988.fst(21,32-21,38): - Prims.string is not a subtype of the expected type _: (*?u21*) _ -> (*?u22*) _ >>]

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

(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 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 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 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 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 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 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 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 ulib/FStar.Pervasives.fsti:55.0-55.56

(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

(242) * Warning 242 at 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: ulib/FStar.WellFounded.fst:86.12-86.15

(242) * Warning 242 at 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: ulib/FStar.WellFounded.fst:126.12-126.15

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

(330) * Warning 330 at 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 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 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: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

(318) * Warning 318 at 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 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: ulib/FStar.WellFounded.fst:86.12-86.15

(242) * Warning 242 at 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: ulib/FStar.WellFounded.fst:126.12-126.15

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

(318) * Warning 318 at 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 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: ulib/FStar.WellFounded.fst:86.12-86.15

(242) * Warning 242 at 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: ulib/FStar.WellFounded.fst:126.12-126.15

(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

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

time = 0.15

time = 0.18

time = 0.22

time = 0.30

time = 0.47