From f3f7d15cfb2ca329ce2560d8190fdf2d84b683ab Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Wed, 26 Jun 2019 18:39:31 +0530 Subject: [PATCH] interactive tests --- .../backtracking.refinements.out.expected | 16 ++++++++-------- .../integration.push-pop.out.expected | 14 +++++++------- ...mber.interface-violation-and-fix.out.expected | 2 +- .../number.interface-violation.out.expected | 2 +- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/src/tests/interactive/backtracking.refinements.out.expected b/src/tests/interactive/backtracking.refinements.out.expected index 56371566e89..532b1181f82 100644 --- a/src/tests/interactive/backtracking.refinements.out.expected +++ b/src/tests/interactive/backtracking.refinements.out.expected @@ -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": ""}]}], "status": "success"} {"kind": "response", "query-id": "16", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "ranges": [{"beg": [3, 12], "end": [3, 12], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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"} @@ -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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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"} @@ -53,7 +53,7 @@ {"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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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"} @@ -61,12 +61,12 @@ {"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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [3, 14], "end": [3, 19], "fname": ""}]}], "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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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": ""}, {"beg": [5, 13], "end": [5, 18], "fname": ""}]}], "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"} diff --git a/src/tests/interactive/integration.push-pop.out.expected b/src/tests/interactive/integration.push-pop.out.expected index 03d50a12e5b..a0a07033349 100644 --- a/src/tests/interactive/integration.push-pop.out.expected +++ b/src/tests/interactive/integration.push-pop.out.expected @@ -78,17 +78,17 @@ {"kind": "response", "query-id": "80", "response": [], "status": "success"} {"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "Syntax error: Parsing.Parse_error", "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "98", "response": [], "status": "success"} -{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; 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": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int", "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "107", "response": [], "status": "success"} {"kind": "response", "query-id": "108", "response": [], "status": "success"} {"kind": "response", "query-id": "112", "response": null, "status": "success"} {"kind": "response", "query-id": "114", "response": [], "status": "success"} -{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; 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": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int", "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "118", "response": [], "status": "success"} {"kind": "response", "query-id": "119", "response": [], "status": "success"} {"kind": "response", "query-id": "122", "response": null, "status": "success"} {"kind": "response", "query-id": "124", "response": [], "status": "success"} -{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; 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": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int", "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "128", "response": [], "status": "success"} {"kind": "response", "query-id": "130", "response": [], "status": "success"} {"kind": "response", "query-id": "133", "response": [], "status": "success"} @@ -96,20 +96,20 @@ {"kind": "response", "query-id": "159", "response": [{"level": "error", "message": "Expected expression of type \"Type0\"; got expression \"Integration.xx\" of type \"nat\"", "ranges": [{"beg": [13, 15], "end": [13, 20], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "163", "response": [], "status": "success"} {"kind": "response", "query-id": "164", "response": [], "status": "success"} -{"kind": "response", "query-id": "165", "response": [{"level": "error", "message": "assertion failed\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": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} +{"kind": "response", "query-id": "165", "response": [{"level": "error", "message": "assertion failed", "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} {"kind": "response", "query-id": "170", "response": [], "status": "success"} {"kind": "response", "query-id": "175", "response": [{"level": "error", "message": "Unexpected numeric literal. Restart F* to load FStar.UInt8.", "ranges": [{"beg": [13, 22], "end": [13, 24], "fname": ""}]}], "status": "success"} {"kind": "response", "query-id": "179", "response": [], "status": "success"} -{"kind": "response", "query-id": "180", "response": [{"level": "error", "message": "assertion failed\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": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 24], "fname": ""}]}], "status": "failure"} +{"kind": "response", "query-id": "180", "response": [{"level": "error", "message": "assertion failed", "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 24], "fname": ""}]}], "status": "failure"} {"kind": "response", "query-id": "185", "response": [], "status": "success"} {"kind": "response", "query-id": "186", "response": [], "status": "success"} {"kind": "response", "query-id": "191", "response": null, "status": "success"} {"kind": "response", "query-id": "192", "response": null, "status": "success"} {"kind": "response", "query-id": "194", "response": [], "status": "success"} -{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; 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": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} +{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "Subtyping check failed; expected type nat; got type int", "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [441, 17], "end": [441, 23], "fname": "prims.fst"}]}], "status": "failure"} {"kind": "response", "query-id": "200", "response": [], "status": "success"} {"kind": "response", "query-id": "204", "response": [], "status": "success"} -{"kind": "response", "query-id": "205", "response": [{"level": "error", "message": "assertion failed\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": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} +{"kind": "response", "query-id": "205", "response": [{"level": "error", "message": "assertion failed", "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"} {"kind": "response", "query-id": "211", "response": [], "status": "success"} {"kind": "response", "query-id": "213", "response": [], "status": "success"} {"kind": "response", "query-id": "214", "response": [], "status": "success"} diff --git a/src/tests/interactive/number.interface-violation-and-fix.out.expected b/src/tests/interactive/number.interface-violation-and-fix.out.expected index 78b5987d988..91600068fc3 100644 --- a/src/tests/interactive/number.interface-violation-and-fix.out.expected +++ b/src/tests/interactive/number.interface-violation-and-fix.out.expected @@ -1,7 +1,7 @@ {"kind": "protocol-info", "rest": "[...]"} {"kind": "response", "query-id": "1", "response": null, "status": "success"} {"kind": "response", "query-id": "2", "response": [], "status": "success"} -{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: int{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, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"} +{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: int{a > 0}; got type int", "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"} {"kind": "response", "query-id": "4", "response": null, "status": "success"} {"kind": "response", "query-id": "5", "response": null, "status": "success"} {"kind": "response", "query-id": "6", "response": [], "status": "success"} diff --git a/src/tests/interactive/number.interface-violation.out.expected b/src/tests/interactive/number.interface-violation.out.expected index 8e699b3fbc0..e9ab41ba27d 100644 --- a/src/tests/interactive/number.interface-violation.out.expected +++ b/src/tests/interactive/number.interface-violation.out.expected @@ -1,4 +1,4 @@ {"kind": "protocol-info", "rest": "[...]"} {"kind": "response", "query-id": "1", "response": null, "status": "success"} {"kind": "response", "query-id": "2", "response": [], "status": "success"} -{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: int{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, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"} +{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "Subtyping check failed; expected type a: int{a > 0}; got type int", "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"}