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 02:25:32.698166123 +0000 +++ AQualMismatch.fst.output.expected 2025-03-04 02:23:02.420416369 +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 02:25:33.073170351 +0000 +++ AnotType.fst.output.expected 2025-03-04 02:23:02.420416369 +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 02:25:33.397174003 +0000 +++ ArgsAndQuals.fst.output.expected 2025-03-04 02:23:02.420416369 +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 02:25:33.738177848 +0000 +++ ArgsMismatch.fst.output.expected 2025-03-04 02:23:02.420416369 +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 02:25:34.234183440 +0000 +++ ArrowRanges.fst.output.expected 2025-03-04 02:23:02.420416369 +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 02:25:34.654188175 +0000 +++ AssertNorm.fst.output.expected 2025-03-04 02:23:02.421416380 +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 02:25:35.124193473 +0000 +++ Asserts.fst.output.expected 2025-03-04 02:23:02.421416380 +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 02:25:35.466197329 +0000 +++ BadEmptyRecord.fst.output.expected 2025-03-04 02:23:02.421416380 +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 02:25:36.056203981 +0000 +++ Basic.fst.output.expected 2025-03-04 02:23:02.421416380 +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 02:25:36.933213868 +0000 +++ Bug1918.fst.output.expected 2025-03-04 02:23:02.421416380 +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) >>]

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