Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

Process completed with exit code 2.

Diff failed for files /bare-tests/_output/Check.fst.output and /bare-tests/Check.fst.output.expected: --- Check.fst.output.expected 2025-12-17 04:13:26.000000000 +0000 +++ _output/Check.fst.output 2025-12-17 04:34:53.346236691 +0000 @@ -1,9 +1,9 @@ -* Info at Check.fst(5,0-5,8): +* Info at Check.fst:5.1-5.9: - Term 1 has type Prims.int -* Info at Check.fst(6,0-6,10): +* Info at Check.fst:6.1-6.11: - Term 1 + 1 has type Prims.int -* Info at Check.fst(11,0-11,10): +* Info at Check.fst:11.1-11.11: - Term Check.foo has type Prims.Tot (#_: Type -> x: _ -> Prims.Tot _)

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`

Process completed with exit code 1.

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1994,4-1994,12): - Global binding 'FStarC.Parser.ToDocument.p_tmNoEq' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1730,4-1730,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body

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

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

(271) * Warning 271 at /__w/FStar/FStar/FStar/stage0/out/lib/fstar/ulib/FStar.UInt.fsti(436,8-436,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst:284.16-284.18: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst:284.16-284.18) and t1 (bound in Pulse.Syntax.Base.fst:173.21-173.23) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst:289.15-289.17: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of q1 (bound in Pulse.Syntax.Base.fst:289.15-289.17) and t1 (bound in Pulse.Syntax.Base.fst:173.21-173.23) are equal. - The type of the first term is: Pulse.Syntax.Base.qualifier - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst:123.21-123.23: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in Pulse.Syntax.Base.fst:123.21-123.23) and pb1 (bound in Pulse.Syntax.Base.fst:139.17-139.20) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst:139.17-139.20: - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in Pulse.Syntax.Base.fst:139.17-139.20) and p1 (bound in Pulse.Syntax.Base.fst:123.21-123.23) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool - The type of the second term is: Pulse.Syntax.Base.pattern - If the proof fails, try annotating these with the same type.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst:882.5-882.17: - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:601.48-601.49: - 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/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:600.48-600.49: - 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 '@'.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:497.9-497.18: - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst:359.9-359.16: - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/checker/Pulse.Common.fst:84.12-84.13: - 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 '@'.

(344) * Warning 344 at /__w/FStar/FStar/FStar/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 /__w/FStar/FStar/FStar/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 /__w/FStar/FStar/FStar/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.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 /__w/FStar/FStar/FStar/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 /__w/FStar/FStar/FStar/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.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 /__w/FStar/FStar/FStar/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 /__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 /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti:55.1-55.57

(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti:645.67-645.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:645.56-645.57

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:26.5-26.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.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.

(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/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

(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/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

(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/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

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst:296.9-296.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:436.9-436.52

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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/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.

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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:26.5-26.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:26.5-26.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.

(352) * Warning 352 at /home/runner/work/FStar/FStar/fstar/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 /home/runner/work/FStar/FStar/fstar/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.

(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/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

(330) * Warning 330 at /home/runner/work/FStar/FStar/fstar/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

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/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.

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst:296.9-296.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:436.9-436.52

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:436.9-436.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.fsti:436.9-436.52: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.TSet.fst:26.5-26.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.

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

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

time = 0.88

time = 0.50

time = 0.32

time = 0.23

time = 0.18

time = 0.16