diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-31 18:12:16 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 18:12:16 -0700 |
| commit | cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 (patch) | |
| tree | e69411603787d99cea12d729ec0a0a2ae8889f20 /test/regress/regress0 | |
| parent | 186b3872a3de454d0f30224dc2e0a396163c3fdc (diff) | |
Rename checkValid/query to checkEntailed. (#4191)
This renames api::Solver::checkValidAssuming to checkEntailed and
removes api::Solver::checkValid. Internally, SmtEngine::query is renamed
to SmtEngine::checkEntailed, and these changes are further propagated to
the Result class.
Diffstat (limited to 'test/regress/regress0')
120 files changed, 145 insertions, 145 deletions
diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc index 1de397ab1..08d591590 100644 --- a/test/regress/regress0/arith/arith.01.cvc +++ b/test/regress/regress0/arith/arith.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc index d7b0291f7..e0a48c357 100644 --- a/test/regress/regress0/arith/arith.02.cvc +++ b/test/regress/regress0/arith/arith.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; z : REAL; diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc index 288c341ef..ce54c8b7e 100644 --- a/test/regress/regress0/arith/arith.03.cvc +++ b/test/regress/regress0/arith/arith.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc index 54df5e62c..bfb3e75d5 100644 --- a/test/regress/regress0/arith/bug549.cvc +++ b/test/regress/regress0/arith/bug549.cvc @@ -1,3 +1,3 @@ -% EXPECT: valid +% EXPECT: entailed a, b : REAL; -QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a;
\ No newline at end of file +QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a; diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc index 265d18a84..84954a3ea 100644 --- a/test/regress/regress0/arith/integers/arith-int-014.cvc +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc index d2e2639ab..8f8b01fc9 100644 --- a/test/regress/regress0/arith/integers/arith-int-015.cvc +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc index 345c90899..66f02401b 100644 --- a/test/regress/regress0/arith/integers/arith-int-021.cvc +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc index 01d51a226..b3d79e8ff 100644 --- a/test/regress/regress0/arith/integers/arith-int-023.cvc +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc index 5a11212d5..e905da9a0 100644 --- a/test/regress/regress0/arith/integers/arith-int-025.cvc +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc index c38231695..b6db26e86 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc index 77571e526..3fd20a0b6 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x1: INT; x0: INT; QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc index 7fa2fc937..1739b3364 100644 --- a/test/regress/regress0/arith/integers/arith-int-079.cvc +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc index d79ec94a7..ed6cb747e 100644 --- a/test/regress/regress0/arith/integers/arith-interval.cvc +++ b/test/regress/regress0/arith/integers/arith-interval.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x: INT; P: INT -> BOOLEAN; diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index 9d1029cbf..07a2aa2f5 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/bug310.cvc b/test/regress/regress0/bug310.cvc index 0cb6cf0fe..12cb80494 100644 --- a/test/regress/regress0/bug310.cvc +++ b/test/regress/regress0/bug310.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed b : BOOLEAN; DATATYPE D = c(s:INT) END; QUERY c(IF b THEN 1 ELSE 0 ENDIF) = IF b THEN c(1) ELSE c(0) ENDIF; diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index 304dd6ec4..400f55885 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a:BOOLEAN; b:BOOLEAN; ASSERT(a); diff --git a/test/regress/regress0/bug322b.cvc b/test/regress/regress0/bug322b.cvc index fa9462f64..0e06cbc13 100644 --- a/test/regress/regress0/bug322b.cvc +++ b/test/regress/regress0/bug322b.cvc @@ -1,7 +1,7 @@ % COMMAND-LINE: --incremental -% EXPECT: valid -% EXPECT: valid -% EXPECT: valid +% EXPECT: entailed +% EXPECT: entailed +% EXPECT: entailed x : INT; y : INT = x + 1; z : INT = -10; diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc index c51af4e24..665bcdafb 100644 --- a/test/regress/regress0/bug486.cvc +++ b/test/regress/regress0/bug486.cvc @@ -1,6 +1,6 @@ % COMMAND-LINE: --finite-model-find -i -% EXPECT: invalid -% EXPECT: valid +% EXPECT: not_entailed +% EXPECT: entailed prin:TYPE; form:TYPE; diff --git a/test/regress/regress0/bv/bvcomp.cvc b/test/regress/regress0/bv/bvcomp.cvc index b9b4b8e17..17064a2f2 100644 --- a/test/regress/regress0/bv/bvcomp.cvc +++ b/test/regress/regress0/bv/bvcomp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x : BITVECTOR(10); diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index dcacd643a..6bc649a03 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Some tests from the CVC3 user manual. % http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html diff --git a/test/regress/regress0/cvc-rerror-print.cvc b/test/regress/regress0/cvc-rerror-print.cvc index dd05723d2..e134b5666 100644 --- a/test/regress/regress0/cvc-rerror-print.cvc +++ b/test/regress/regress0/cvc-rerror-print.cvc @@ -1,5 +1,5 @@ -% EXPECT: valid -% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response. +% EXPECT: entailed +% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response. OPTION "logic" "ALL"; OPTION "produce-models" true; x : INT; diff --git a/test/regress/regress0/cvc3-bug15.cvc b/test/regress/regress0/cvc3-bug15.cvc index 860ce38bd..779a2eab4 100644 --- a/test/regress/regress0/cvc3-bug15.cvc +++ b/test/regress/regress0/cvc3-bug15.cvc @@ -1,5 +1,5 @@ %% This test borrowed from CVC3 regressions, bug15.cvc -% EXPECT: valid +% EXPECT: entailed x : REAL; y : REAL; f : REAL -> REAL; diff --git a/test/regress/regress0/cvc3.userdoc.01.cvc b/test/regress/regress0/cvc3.userdoc.01.cvc index 7c89de4ac..e3e9aaf0a 100644 --- a/test/regress/regress0/cvc3.userdoc.01.cvc +++ b/test/regress/regress0/cvc3.userdoc.01.cvc @@ -1,31 +1,31 @@ % COMMAND-LINE: --incremental -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0000111101010000 = 0hex0f50; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin01@0bin0 = 0bin010; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011[3:1] = 0bin001; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011 << 3 = 0bin0011000; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin1000 >> 3 = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY SX(0bin100, 5) = 0bin11100; -% EXPECT: valid +% EXPECT: entailed QUERY BVZEROEXTEND(0bin1,3) = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY BVREPEAT(0bin10,3) = 0bin101010; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTL(0bin101,1) = 0bin011; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTR(0bin101,1) = 0bin110; diff --git a/test/regress/regress0/cvc3.userdoc.02.cvc b/test/regress/regress0/cvc3.userdoc.02.cvc index b6329e953..e143ea275 100644 --- a/test/regress/regress0/cvc3.userdoc.02.cvc +++ b/test/regress/regress0/cvc3.userdoc.02.cvc @@ -2,6 +2,6 @@ x : BITVECTOR(5); y : BITVECTOR(4); yy : BITVECTOR(3); -% EXPECT: valid +% EXPECT: entailed QUERY BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ; diff --git a/test/regress/regress0/cvc3.userdoc.03.cvc b/test/regress/regress0/cvc3.userdoc.03.cvc index 4fc6a5f8c..3b3829ebc 100644 --- a/test/regress/regress0/cvc3.userdoc.03.cvc +++ b/test/regress/regress0/cvc3.userdoc.03.cvc @@ -1,7 +1,7 @@ bv : BITVECTOR(10); a : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] AND diff --git a/test/regress/regress0/cvc3.userdoc.04.cvc b/test/regress/regress0/cvc3.userdoc.04.cvc index 824690bcf..da8b1e82c 100644 --- a/test/regress/regress0/cvc3.userdoc.04.cvc +++ b/test/regress/regress0/cvc3.userdoc.04.cvc @@ -5,5 +5,5 @@ ASSERT x&y&t&z&q = x; ASSERT x|y = t; ASSERT BVXOR(x,~x) = t; -% EXPECT: valid +% EXPECT: entailed QUERY FALSE; diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc index 37da96b3c..85e0c2105 100644 --- a/test/regress/regress0/cvc3.userdoc.05.cvc +++ b/test/regress/regress0/cvc3.userdoc.05.cvc @@ -3,7 +3,7 @@ x, y : BITVECTOR(4); ASSERT x = 0hex5; ASSERT y = 0bin0101; -% EXPECT: valid +% EXPECT: entailed QUERY BVMULT(8,x,y)=BVMULT(8,y,x) AND diff --git a/test/regress/regress0/cvc3.userdoc.06.cvc b/test/regress/regress0/cvc3.userdoc.06.cvc index 3801b6d53..3968365ad 100644 --- a/test/regress/regress0/cvc3.userdoc.06.cvc +++ b/test/regress/regress0/cvc3.userdoc.06.cvc @@ -6,8 +6,8 @@ z, t : BITVECTOR(12); ASSERT x = 0hexff; ASSERT z = 0hexff0; -% EXPECT: valid +% EXPECT: entailed QUERY z = x << 4; -% EXPECT: valid +% EXPECT: entailed QUERY (z >> 4)[7:0] = x; diff --git a/test/regress/regress0/datatypes/bug286.cvc b/test/regress/regress0/datatypes/bug286.cvc index 501f5f737..33a320acd 100644 --- a/test/regress/regress0/datatypes/bug286.cvc +++ b/test/regress/regress0/datatypes/bug286.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE foo = f(i:INT) END; x : foo; y : INT; diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc index 8e2818106..e28fc6305 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc +++ b/test/regress/regress0/datatypes/datatype-dump.cvc @@ -10,7 +10,7 @@ % EXPECT: END; % EXPECT: x : nat; % EXPECT: QUERY NOT(is_succ(x)) AND NOT(is_zero(x)); -% EXPECT: invalid +% EXPECT: not_entailed % DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype.cvc b/test/regress/regress0/datatypes/datatype.cvc index 20fec4fdd..6a0e97fc3 100644 --- a/test/regress/regress0/datatypes/datatype.cvc +++ b/test/regress/regress0/datatypes/datatype.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype0.cvc b/test/regress/regress0/datatypes/datatype0.cvc index 8fff50a86..0b9e41024 100644 --- a/test/regress/regress0/datatypes/datatype0.cvc +++ b/test/regress/regress0/datatypes/datatype0.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc index 3934959f1..9e746c0e4 100644 --- a/test/regress/regress0/datatypes/datatype1.cvc +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype13.cvc b/test/regress/regress0/datatypes/datatype13.cvc index 91e582dbd..78d28be00 100644 --- a/test/regress/regress0/datatypes/datatype13.cvc +++ b/test/regress/regress0/datatypes/datatype13.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE enum = enum1 | enum2 diff --git a/test/regress/regress0/datatypes/datatype2.cvc b/test/regress/regress0/datatypes/datatype2.cvc index 939dff197..64c84de45 100644 --- a/test/regress/regress0/datatypes/datatype2.cvc +++ b/test/regress/regress0/datatypes/datatype2.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc index fff1a5dd7..ce99edbb7 100644 --- a/test/regress/regress0/datatypes/datatype3.cvc +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE tree = node(left : tree, right : tree) | leaf diff --git a/test/regress/regress0/datatypes/datatype4.cvc b/test/regress/regress0/datatypes/datatype4.cvc index 217777bdf..83962f49a 100644 --- a/test/regress/regress0/datatypes/datatype4.cvc +++ b/test/regress/regress0/datatypes/datatype4.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE TypeGeneric = generic END; diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 4f6320028..b6950845e 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -7,15 +7,15 @@ b1, b2 : [##]; % empty records (a unit type) c1, c2 : [[]]; % 1-tuples of the empty tuple (a unit type) d1, d2 : [#x:[[##]],y:[#z:[]#]#]; % more complicated records (still a unit type) -% EXPECT: valid +% EXPECT: entailed QUERY a1 = a2; -% EXPECT: valid +% EXPECT: entailed QUERY b1 = b2; -% EXPECT: valid +% EXPECT: entailed QUERY c1 = c2; -% EXPECT: valid +% EXPECT: entailed QUERY d1 = d2; diff --git a/test/regress/regress0/datatypes/mutually-recursive.cvc b/test/regress/regress0/datatypes/mutually-recursive.cvc index b86b647b5..5bd857b6e 100644 --- a/test/regress/regress0/datatypes/mutually-recursive.cvc +++ b/test/regress/regress0/datatypes/mutually-recursive.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat2) | zero, nat2 = succ2(pred2 : nat) | zero2 END; diff --git a/test/regress/regress0/datatypes/rec1.cvc b/test/regress/regress0/datatypes/rec1.cvc index 79c9facda..b3e205985 100644 --- a/test/regress/regress0/datatypes/rec1.cvc +++ b/test/regress/regress0/datatypes/rec1.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed c : BOOLEAN; a17 : BOOLEAN = ((# _a := 2, _b := 2 #) = ( IF c THEN (# _a := 3, _b := 2 #) diff --git a/test/regress/regress0/datatypes/rec2.cvc b/test/regress/regress0/datatypes/rec2.cvc index 44d523a46..56864c088 100644 --- a/test/regress/regress0/datatypes/rec2.cvc +++ b/test/regress/regress0/datatypes/rec2.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed c : BOOLEAN; a16 : [# _a : INT, _b : INT #] = ( IF c THEN (# _a := 3, _b := 2 #) diff --git a/test/regress/regress0/datatypes/rec4.cvc b/test/regress/regress0/datatypes/rec4.cvc index 08a9988ef..f7f29755f 100644 --- a/test/regress/regress0/datatypes/rec4.cvc +++ b/test/regress/regress0/datatypes/rec4.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a : BOOLEAN; a49 : BOOLEAN = ( IF a THEN (# _a := 1 #) diff --git a/test/regress/regress0/datatypes/rewriter.cvc b/test/regress/regress0/datatypes/rewriter.cvc index 18f8b3441..e9b7662a0 100644 --- a/test/regress/regress0/datatypes/rewriter.cvc +++ b/test/regress/regress0/datatypes/rewriter.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % simple test for rewriter cases diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc b/test/regress/regress0/datatypes/tuple-record-bug.cvc index 33c68dece..0e519a64f 100644 --- a/test/regress/regress0/datatypes/tuple-record-bug.cvc +++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed Mem_0 : TYPE = ARRAY INT OF INT; diff --git a/test/regress/regress0/datatypes/tuple.cvc b/test/regress/regress0/datatypes/tuple.cvc index 366737525..00ab8d4db 100644 --- a/test/regress/regress0/datatypes/tuple.cvc +++ b/test/regress/regress0/datatypes/tuple.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x: [REAL,INT,REAL] = ( 4/5, 9, 11/9 ); first_elem: REAL = x.0; third_elem: REAL = x.2; diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc index ee414ed65..72c23d888 100644 --- a/test/regress/regress0/datatypes/typed_v10l30054.cvc +++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc index 988646f21..95b1a935f 100644 --- a/test/regress/regress0/datatypes/typed_v1l80005.cvc +++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc index f32c9e551..2295d1518 100644 --- a/test/regress/regress0/datatypes/typed_v2l30079.cvc +++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc index c6260e233..e067852df 100644 --- a/test/regress/regress0/datatypes/typed_v3l20092.cvc +++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc index 05d0247cc..f980acc69 100644 --- a/test/regress/regress0/datatypes/typed_v5l30069.cvc +++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc index 7b2da4b65..257bf2ccc 100644 --- a/test/regress/regress0/datatypes/v10l40099.cvc +++ b/test/regress/regress0/datatypes/v10l40099.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc index fc466f300..d3411e12e 100644 --- a/test/regress/regress0/datatypes/v2l40025.cvc +++ b/test/regress/regress0/datatypes/v2l40025.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index b7019e7ae..ea27672d5 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc index be101b8fb..d3db742ae 100644 --- a/test/regress/regress0/datatypes/v5l30058.cvc +++ b/test/regress/regress0/datatypes/v5l30058.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, list = cons(car : tree, cdr : list) | null, diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc index b0dbdc46e..67be78912 100644 --- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc +++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero END; diff --git a/test/regress/regress0/fmf/bug-041417-set-options.cvc b/test/regress/regress0/fmf/bug-041417-set-options.cvc index 16f59f78c..c4e9ba834 100644 --- a/test/regress/regress0/fmf/bug-041417-set-options.cvc +++ b/test/regress/regress0/fmf/bug-041417-set-options.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed OPTION "finite-model-find"; OPTION "fmf-fun"; diff --git a/test/regress/regress0/let.cvc b/test/regress/regress0/let.cvc index 996b09d39..d0f5c5e1f 100644 --- a/test/regress/regress0/let.cvc +++ b/test/regress/regress0/let.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed U: TYPE; a: U; b: U; diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index 2c2ac2f79..305f2d396 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index 67415e95d..c74c11983 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: invalid +% EXPECT: not_entailed QUERY NOT c AND b; diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 42298a8f4..1c86ce594 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index 89a9db320..254b0ed87 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,3 +1,3 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a => b) <=> (NOT a OR b); diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 1ec94e5ae..2897dbc0c 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY TRUE XOR FALSE; diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index 5115a90c1..3ede8d211 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND and NOT. A, B: BOOLEAN; diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc index 879becbbf..ec69087d1 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc index b8729e92a..4f81c86ad 100644 --- a/test/regress/regress0/precedence/bool-cmp.cvc +++ b/test/regress/regress0/precedence/bool-cmp.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of comparisons and booleans x , y, z: INT; diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc index a7c07fe30..54ee7b8f8 100644 --- a/test/regress/regress0/precedence/cmp-plus.cvc +++ b/test/regress/regress0/precedence/cmp-plus.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of comparisons and plus/minus x, y, z: INT; diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc index 9e581d514..af81ea10d 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of function application and = T : TYPE; diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc index 745cc7474..4643292b6 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right associativity of <=> A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc index 947433c88..24181487d 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc index 1a7cef3b1..c6883c6ad 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right associativity of => A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc index 3de26eb18..9ebed72d4 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of <=> and =>. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc index d724d33ef..883e7d4a1 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc index fc671d7b5..579531ded 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of AND and NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc index f658c127e..f8c7366be 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of = and NOT. A, B: INT; diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc index 209df8559..746f142e4 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of => and OR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 2a25bac63..405cb68b7 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc index 5d980f90d..57b9b99cf 100644 --- a/test/regress/regress0/precedence/plus-mult.cvc +++ b/test/regress/regress0/precedence/plus-mult.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of plus/minus and mult/divide a, b, c, d, e: INT; diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc index 68896db10..08c939c5e 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of XOR and AND. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc index f31324a53..5f4646b1f 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for left associativity of XOR A, B, C: BOOLEAN; diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc index 757286764..87abc0e73 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc index c86843535..2e51a42ad 100644 --- a/test/regress/regress0/preprocess/preprocess_00.cvc +++ b/test/regress/regress0/preprocess/preprocess_00.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc index e2c93a359..0f94103f6 100644 --- a/test/regress/regress0/preprocess/preprocess_02.cvc +++ b/test/regress/regress0/preprocess/preprocess_02.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc index 3e45c529a..abcc7a6ac 100644 --- a/test/regress/regress0/preprocess/preprocess_06.cvc +++ b/test/regress/regress0/preprocess/preprocess_06.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5: BOOLEAN; diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc index 8b26c0d08..9a6cd797c 100644 --- a/test/regress/regress0/preprocess/preprocess_13.cvc +++ b/test/regress/regress0/preprocess/preprocess_13.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc index 267a316e8..966668002 100644 --- a/test/regress/regress0/printer/tuples_and_records.cvc +++ b/test/regress/regress0/printer/tuples_and_records.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed % EXPECT: ((r.a, "active")) % EXPECT: ((y.1, 9)) OPTION "produce-models"; diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc index 2b9eedcdb..1a6049329 100644 --- a/test/regress/regress0/push-pop/bug233.cvc +++ b/test/regress/regress0/push-pop/bug233.cvc @@ -3,9 +3,9 @@ a, b: BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY (a AND b) OR NOT (a AND b); -% EXPECT: invalid +% EXPECT: not_entailed QUERY (a OR b); diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc index 9b10ef843..657e74486 100644 --- a/test/regress/regress0/push-pop/incremental-subst-bug.cvc +++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc @@ -1,21 +1,21 @@ % COMMAND-LINE: --incremental U : TYPE; x, y : U; -% EXPECT: invalid +% EXPECT: not_entailed QUERY x = y; ASSERT x = y; -% EXPECT: valid +% EXPECT: entailed QUERY x = y; PUSH; z : U; -% EXPECT: valid +% EXPECT: entailed QUERY x = y; -% EXPECT: invalid +% EXPECT: not_entailed QUERY x = z; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z = x; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z /= x; POP; -% EXPECT: invalid +% EXPECT: not_entailed QUERY z /= x; diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc index 63cf52fd6..d01d7b7d2 100644 --- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -1,2 +1,2 @@ -% EXPECT: valid +% EXPECT: entailed QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc index 6740faa8c..06d2b5049 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc +++ b/test/regress/regress0/sets/cvc-sample.cvc @@ -4,7 +4,7 @@ % EXPECT: unsat % EXPECT: unsat % EXPECT: unsat -% EXPECT: invalid +% EXPECT: not_entailed OPTION "incremental" true; OPTION "logic" "ALL_SUPPORTED"; SetInt : TYPE = SET OF INT; diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index 83d0225bd..def48254e 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -3,5 +3,5 @@ ASSERT x1 OR NOT x0; ASSERT x0 OR NOT x3; ASSERT x3 OR x2; ASSERT x1 AND NOT x1; -% EXPECT: valid +% EXPECT: entailed QUERY x2; diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index bd732b4dc..dcb7c6f0d 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -4,6 +4,6 @@ ASSERT NOT a OR NOT b; ASSERT c OR b OR a; ASSERT b OR NOT a; ASSERT a OR NOT b OR c; -% EXPECT: invalid +% EXPECT: not_entailed QUERY FALSE; diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2 index 489d686b3..4bfa1766a 100644 --- a/test/regress/regress0/smtlib/set-info-status.smt2 +++ b/test/regress/regress0/smtlib/set-info-status.smt2 @@ -1,4 +1,4 @@ -; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.") +; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/ENTAILED response.") ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 45052deeb..26dda442e 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -3,5 +3,5 @@ x, y : BOOLEAN; ASSERT (x OR y); ASSERT NOT (x OR y); -% EXPECT: valid +% EXPECT: entailed QUERY FALSE; diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index bfe1a3285..7872f5a1a 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc index 42b99cc44..6b0f93324 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc index 1dd96fd1c..2bd0b1e1e 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc index cc1721ca6..15fe5907c 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc index 66223ca7b..0fc52bcca 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index 9de754284..b25d8a471 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc index fb38fab65..1516503ff 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (b OR c) <=> (a OR b) OR c; diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index 93d555c96..ebeadee14 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (b AND c) <=> (a AND b) AND c; diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 08b049c17..ca0e6a8d1 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR b <=> b OR a; diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index b88de6144..75fe17238 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND b <=> b AND a; diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index 0fe647f7b..2f87e4ca0 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (a AND b) <=> a; diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 1d466a86e..a4075bda3 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (a OR b) <=> a; diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index 146d92832..3b4527bdc 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index e9c7d3fa3..e15a21412 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index 478be2db9..5bc5faca5 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR NOT a; diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index 226a3da82..613022e84 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND NOT a <=> FALSE; diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index d615fef3b..8debef9cd 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR a <=> a; diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index 209e512a6..2274fc78e 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND a <=> a; diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 2cc69f048..80b95802d 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR FALSE <=> a; diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 5a6c16248..7b8a14edb 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND TRUE <=> a; diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index 6dc84f679..dfb4f13fc 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a OR TRUE <=> TRUE; diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index 6b2bf4113..9c69baa52 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY a AND FALSE <=> FALSE; diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index 7c6701acc..c58160bb9 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT FALSE <=> TRUE; diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 7c1b1b8e4..17773b899 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT TRUE <=> FALSE; diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index d5812b5ea..46b6fc02e 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT (a OR b) <=> NOT a AND NOT b; diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 8d2570620..42e114010 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT (a AND b) <=> NOT a OR NOT b; diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index d65cbcf65..bcc69beea 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -1,4 +1,4 @@ a, b, c : BOOLEAN; -% EXPECT: valid +% EXPECT: entailed QUERY NOT NOT a <=> a; |