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*) _ >>]

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