Diff failed for files /tests/error-messages/_output/ArgsMismatch.fst.json_output and /tests/error-messages/ArgsMismatch.fst.json_output.expected: --- ArgsMismatch.fst.json_output.expected 2025-12-17 04:33:14.786629385 +0000 +++ _output/ArgsMismatch.fst.json_output 2025-12-17 04:37:18.922090284 +0000 @@ -1,12 +1,12 @@ -{"msg":["Expected failure:","Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":7,"col":33},"end_pos":{"line":7,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":7,"col":33},"end_pos":{"line":7,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} -{"msg":["Expected failure:","Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":8,"col":35},"end_pos":{"line":8,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":8,"col":35},"end_pos":{"line":8,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]} -{"msg":["Expected failure:","Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":10,"col":34},"end_pos":{"line":10,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":10,"col":34},"end_pos":{"line":10,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]} -{"msg":["Expected failure:","Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":14,"col":33},"end_pos":{"line":14,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":14,"col":33},"end_pos":{"line":14,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]} -{"msg":["Expected failure:","Inconsistent argument qualifiers.","Expected an implicit argument, got an explicit one."],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":15,"col":35},"end_pos":{"line":15,"col":36}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":15,"col":35},"end_pos":{"line":15,"col":36}}},"number":92,"ctx":["While typechecking the top-level declaration `let uu___1`","While typechecking the top-level declaration `[@@expect_failure] let uu___1`"]} -{"msg":["Expected failure:","Too many arguments to function of type y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":17,"col":34},"end_pos":{"line":17,"col":35}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":17,"col":34},"end_pos":{"line":17,"col":35}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]} -{"msg":["Expected failure:","Too many arguments to function of type [@@@ 2]y: Prims.int -> Prims.int","Got\n2\narguments","Remaining type is Prims.int"],"level":"Info","range":{"def":{"file_name":"ArgsMismatch.fst","start_pos":{"line":21,"col":33},"end_pos":{"line":21,"col":34}},"use":{"file_name":"ArgsMismatch.fst","start_pos":{"line":21,"col":33},"end_pos":{"line":21,"col":34}}},"number":173,"ctx":["While typechecking the top-level declaration `let uu___2`","While typechecking the top-level declaration `[@@expect_failure] let uu___2`"]} -{"msg":["Expected failure:","Inconsistent argument qualifie

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.output and /tests/error-messages/ArgsAndQuals.fst.output.expected: --- ArgsAndQuals.fst.output.expected 2025-12-17 04:33:14.786629385 +0000 +++ _output/ArgsAndQuals.fst.output 2025-12-17 04:37:18.660089797 +0000 @@ -1,13 +1,13 @@ -* Info at ArgsAndQuals.fst(25,16-25,18): +* Info at ArgsAndQuals.fst:25.17-25.19: - Expected failure: - Inconsistent implicit argument annotation on argument uu___ - Got: '#' - Expected: '$' -* Warning 240 at ArgsAndQuals.fst(23,4-23,9): +* Warning 240 at ArgsAndQuals.fst:23.5-23.10: - 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.1-25.30: - Missing definitions in module ArgsAndQuals: test1

Diff failed for files /tests/error-messages/_output/ArgsAndQuals.fst.json_output and /tests/error-messages/ArgsAndQuals.fst.json_output.expected: --- ArgsAndQuals.fst.json_output.expected 2025-12-17 04:33:14.786629385 +0000 +++ _output/ArgsAndQuals.fst.json_output 2025-12-17 04:37:18.438089385 +0000 @@ -1,3 +1,3 @@ -{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Info","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":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":[]} -{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]} +{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument uu___","Got: '#'","Expected: '$'"],"level":"Info","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":["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":[]} +{"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":1},"end_pos":{"line":25,"col":30}}},"number":240,"ctx":[]}

Diff failed for files /tests/error-messages/_output/AnotType.fst.output and /tests/error-messages/AnotType.fst.output.expected: --- AnotType.fst.output.expected 2025-12-17 04:33:14.785629383 +0000 +++ _output/AnotType.fst.output 2025-12-17 04:37:18.175088897 +0000 @@ -1,9 +1,9 @@ -* Info at AnotType.fst(19,5-19,7): +* Info at AnotType.fst:19.6-19.8: - Expected failure: - Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it is eqtype but contains noeq/unopteq qualifiers -* Info at AnotType.fst(27,14-27,16): +* Info at AnotType.fst:27.15-27.17: - Expected failure: - Expected expression of type Type0 got expression tb of type Type

Diff failed for files /tests/error-messages/_output/AnotType.fst.json_output and /tests/error-messages/AnotType.fst.json_output.expected: --- AnotType.fst.json_output.expected 2025-12-17 04:33:14.785629383 +0000 +++ _output/AnotType.fst.json_output 2025-12-17 04:37:17.892088371 +0000 @@ -1,2 +1,2 @@ -{"msg":["Expected failure:","Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Info","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`"]} -{"msg":["Expected failure:","Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Info","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`"]} +{"msg":["Expected failure:","Type annotation Prims.int for inductive AnotType.tc is not Type or eqtype, or it\nis eqtype but contains noeq/unopteq qualifiers"],"level":"Info","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":["Expected failure:","Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Info","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`"]}

Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.output and /tests/error-messages/AQualMismatch.fst.output.expected: --- AQualMismatch.fst.output.expected 2025-12-17 04:33:14.785629383 +0000 +++ _output/AQualMismatch.fst.output 2025-12-17 04:37:17.653087928 +0000 @@ -1,13 +1,13 @@ -* Info at AQualMismatch.fst(6,7-6,8): +* Info at AQualMismatch.fst:6.8-6.9: - Expected failure: - Inconsistent implicit argument annotation on argument x - Got: '#' - Expected: '' -* Warning 240 at AQualMismatch.fst(3,4-3,5): +* Warning 240 at AQualMismatch.fst:3.5-3.6: - 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.1-6.13: - Missing definitions in module AQualMismatch: f

Diff failed for files /tests/error-messages/_output/AQualMismatch.fst.json_output and /tests/error-messages/AQualMismatch.fst.json_output.expected: --- AQualMismatch.fst.json_output.expected 2025-12-17 04:33:14.785629383 +0000 +++ _output/AQualMismatch.fst.json_output 2025-12-17 04:37:17.428087510 +0000 @@ -1,3 +1,3 @@ -{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Info","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":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":[]} -{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]} +{"msg":["Expected failure:","Inconsistent implicit argument annotation on argument x","Got: '#'","Expected: ''"],"level":"Info","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":["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":[]} +{"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":1},"end_pos":{"line":6,"col":13}}},"number":240,"ctx":[]}

Diff failed for files /tests/bug-reports/closed/_output/Bug3980.fst.output and /tests/bug-reports/closed/Bug3980.fst.output.expected: --- Bug3980.fst.output.expected 2025-12-17 04:33:14.775629365 +0000 +++ _output/Bug3980.fst.output 2025-12-17 04:38:11.662179664 +0000 @@ -1,26 +1,26 @@ -* Info at Bug3980.fst(16,0-16,24): +* Info at Bug3980.fst:16.1-16.25: - Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop -* Info at Bug3980.fst(17,0-17,26): +* Info at Bug3980.fst:17.1-17.27: - Term (Bug3980.p 1 ** Bug3980.p 2) ** Bug3980.p 3 has type Bug3980.slprop -* Info at Bug3980.fst(18,0-18,26): +* Info at Bug3980.fst:18.1-18.27: - Term Bug3980.p 1 ** Bug3980.p 2 ** Bug3980.p 3 has type Bug3980.slprop -* Info at Bug3980.fst(23,8-23,14): +* Info at Bug3980.fst:23.9-23.15: - Expected failure: - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Bug3980.fst(23,15-23,23) + - See also Bug3980.fst:23.16-23.24 -* Info at Bug3980.fst(25,8-25,14): +* Info at Bug3980.fst:25.9-25.15: - Expected failure: - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also Bug3980.fst(25,15-25,23) + - See also Bug3980.fst:25.16-25.24 -* Info at Bug3980.fst(33,0-33,29): +* Info at Bug3980.fst:33.1-33.30: - Term "a" |-> 1 ** "b" |-> 2 has type Bug3980.slprop

Diff failed for files /tests/bug-reports/closed/_output/Bug3757.fst.output and /tests/bug-reports/closed/Bug3757.fst.output.expected: --- Bug3757.fst.output.expected 2025-12-17 04:33:14.775629365 +0000 +++ _output/Bug3757.fst.output 2025-12-17 04:38:10.238177141 +0000 @@ -1,18 +1,18 @@ -* Info at Bug3757.fst(8,4-8,13): +* Info at Bug3757.fst:8.5-8.14: - Expected failure: - Expected a pattern of type Prims.int & Prims.int - Type FStar.Pervasives.Native.tuple2 is not a record type. -* Info at Bug3757.fst(12,28-12,31): +* Info at Bug3757.fst:12.29-12.32: - Expected failure: - Expected an expression of type Prims.int & Prims.bool - Type FStar.Pervasives.Native.tuple2 is not a record type. -* Info at Bug3757.fst(15,15-15,17): +* Info at Bug3757.fst:15.16-15.18: - Expected failure: - Field name _1 could not be resolved. -* Info at Bug3757.fst(21,9-21,11): +* Info at Bug3757.fst:21.10-21.12: - Expected failure: - Field name f1 could not be resolved.

(228) * Error 228 at Bug1952a.fst:15.31-15.34: - Tactic failed - Could not solve typeclass constraint `t c`

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

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

(272) * Warning 272 at Test.fst:21.1-21.32: - Top-level let-bindings must be total; this term may have effects

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

(361) * Warning 361 at AlexOpaque.fst:103.1-125.6: - Some #push-options have not been popped. Current depth is 2.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'uint32' in file "UInt32.fsti, UInt32.fst". - Rename "UInt32.fsti, UInt32.fst" to avoid conflicts.

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

(274) * Warning 274: - Implicitly opening namespace 'fstar.tactics.' shadows module 'typeclasses' in file "Typeclasses.fst". - Rename "Typeclasses.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.list.' shadows module 'pure' in file "Pure.fst". - Rename "Pure.fst" to avoid conflicts.