Skip to content

Commit

Permalink
Update expected output
Browse files Browse the repository at this point in the history
  • Loading branch information
mtzguido committed Jul 8, 2024
1 parent 183ec71 commit 8a8896e
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions tests/ide/emacs/fstarmode_gh73.out.expected
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{"kind": "protocol-info", "rest": "[...]"}
{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [623, 15], "end": [623, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- FStar.Stubs.Reflection.V2.Builtins.term_eq is deprecated\n- Use FStar.Reflection.V2.TermEq.term_eq\n- See also FStar.Stubs.Reflection.V2.Builtins.fsti(167,0-167,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [167, 0], "end": [167, 48], "fname": "FStar.Stubs.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n pattern:\n Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
{"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "- Pattern uses these theory symbols or terms that should not be in an SMT\n pattern:\n Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "4", "response": [], "status": "success"}
{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [109, 12], "end": [109, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- exact failed\n- 1 : int does not exactly solve the goal bool (witness = (*?u[...]*) _)\n- See also FStar.Tactics.V2.Derived.fst(109,12-109,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [109, 12], "end": [109, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
{"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [112, 12], "end": [112, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
{"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "- Tactic failed\n- exact failed\n- 1 : int does not exactly solve the goal bool (witness = (*?u[...]*) _)\n- See also FStar.Tactics.V2.Derived.fst(112,12-112,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [112, 12], "end": [112, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}

0 comments on commit 8a8896e

Please sign in to comment.