Skip to content

Commit

Permalink
interactive tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@aseemr
aseemr committed Jun 26, 2019
1 parent df5d281 commit f3f7d15
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 17 deletions.
16 changes: 8 additions & 8 deletions src/tests/interactive/backtracking.refinements.out.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,15 @@
{"kind": "response", "query-id": "15", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "ranges": [{"beg": [3, 12], "end": [3, 12], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "16", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "ranges": [{"beg": [3, 12], "end": [3, 12], "fname": "<input>"}]}], "status": "success"}
{"kind": "response", "query-id": "17", "response": [], "status": "success"}
{"kind": "response", "query-id": "18", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 2}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "18", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 2}; got type int", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "19", "response": [], "status": "success"}
{"kind": "response", "query-id": "20", "response": [], "status": "success"}
{"kind": "response", "query-id": "21", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 1}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "21", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 1}; got type int", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "22", "response": [], "status": "success"}
{"kind": "response", "query-id": "23", "response": [], "status": "success"}
{"kind": "response", "query-id": "24", "response": null, "status": "success"}
{"kind": "response", "query-id": "25", "response": [], "status": "success"}
{"kind": "response", "query-id": "26", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [3, 23], "end": [3, 25], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "26", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int", "ranges": [{"beg": [3, 23], "end": [3, 25], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "27", "response": [], "status": "success"}
{"kind": "response", "query-id": "28", "response": [], "status": "success"}
{"kind": "response", "query-id": "29", "response": [], "status": "success"}
Expand All @@ -43,7 +43,7 @@
{"kind": "response", "query-id": "42", "response": [], "status": "success"}
{"kind": "response", "query-id": "43", "response": [], "status": "success"}
{"kind": "response", "query-id": "44", "response": [], "status": "success"}
{"kind": "response", "query-id": "45", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "45", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "46", "response": [], "status": "success"}
{"kind": "response", "query-id": "47", "response": [], "status": "success"}
{"kind": "response", "query-id": "48", "response": [], "status": "success"}
Expand All @@ -53,20 +53,20 @@
{"kind": "response", "query-id": "52", "response": [], "status": "success"}
{"kind": "response", "query-id": "53", "response": null, "status": "success"}
{"kind": "response", "query-id": "54", "response": [], "status": "success"}
{"kind": "response", "query-id": "55", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "55", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "56", "response": null, "status": "success"}
{"kind": "response", "query-id": "57", "response": [], "status": "success"}
{"kind": "response", "query-id": "58", "response": [], "status": "success"}
{"kind": "response", "query-id": "59", "response": [], "status": "success"}
{"kind": "response", "query-id": "60", "response": null, "status": "success"}
{"kind": "response", "query-id": "61", "response": null, "status": "success"}
{"kind": "response", "query-id": "62", "response": [], "status": "success"}
{"kind": "response", "query-id": "63", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [3, 23], "end": [3, 25], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "63", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int", "ranges": [{"beg": [3, 23], "end": [3, 25], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "64", "response": [], "status": "success"}
{"kind": "response", "query-id": "65", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "65", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: nat{a > 0}; got type int", "ranges": [{"beg": [3, 23], "end": [3, 24], "fname": "<input>"}, {"beg": [3, 14], "end": [3, 19], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "66", "response": [], "status": "success"}
{"kind": "response", "query-id": "67", "response": [], "status": "success"}
{"kind": "response", "query-id": "68", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int\n\tSMT solver says:\n\tunknown because (incomplete quantifiers) (fuel=8; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=4; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=2);\n\tunknown because (incomplete quantifiers) (fuel=2; ifuel=1);\n\tNote: 'canceled' or 'resource limits reached' means the SMT query timed out, so you might want to increase the rlimit;\n\t'incomplete quantifiers' means a (partial) counterexample was found, so try to spell your proof out in greater detail, increase fuel or ifuel\n\t'unknown' means Z3 provided no further reason for the proof failing", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "68", "response": [{"level": "error", "message": "Subtyping check failed; expected type b: nat{b > 1}; got type int", "ranges": [{"beg": [5, 22], "end": [5, 31], "fname": "<input>"}, {"beg": [5, 13], "end": [5, 18], "fname": "<input>"}]}], "status": "failure"}
{"kind": "response", "query-id": "69", "response": null, "status": "success"}
{"kind": "response", "query-id": "70", "response": [], "status": "success"}
{"kind": "response", "query-id": "71", "response": [], "status": "success"}
Expand Down
Loading

0 comments on commit f3f7d15

Please sign in to comment.