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 | |
| 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')
228 files changed, 331 insertions, 358 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; diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc index 03ed1a6ae..3fd528c11 100644 --- a/test/regress/regress1/arith/arith-int-001.cvc +++ b/test/regress/regress1/arith/arith-int-001.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ; ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc index 849daba79..6cc4b2c5e 100644 --- a/test/regress/regress1/arith/arith-int-002.cvc +++ b/test/regress/regress1/arith/arith-int-002.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ; ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc index 9c060c469..f294babe6 100644 --- a/test/regress/regress1/arith/arith-int-003.cvc +++ b/test/regress/regress1/arith/arith-int-003.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ; ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-004.cvc b/test/regress/regress1/arith/arith-int-004.cvc index 314b76d18..15b060d92 100644 --- a/test/regress/regress1/arith/arith-int-004.cvc +++ b/test/regress/regress1/arith/arith-int-004.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc index 9b9776ad3..3701d60b4 100644 --- a/test/regress/regress1/arith/arith-int-005.cvc +++ b/test/regress/regress1/arith/arith-int-005.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ; ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc index 999b4a5b4..53a80310a 100644 --- a/test/regress/regress1/arith/arith-int-006.cvc +++ b/test/regress/regress1/arith/arith-int-006.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ; ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc index 4cb4d88ef..c0732e2b2 100644 --- a/test/regress/regress1/arith/arith-int-007.cvc +++ b/test/regress/regress1/arith/arith-int-007.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ; ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc index 1ae22c993..1810d6f28 100644 --- a/test/regress/regress1/arith/arith-int-008.cvc +++ b/test/regress/regress1/arith/arith-int-008.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ; ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc index 9bd7a2ce4..14b26da6c 100644 --- a/test/regress/regress1/arith/arith-int-009.cvc +++ b/test/regress/regress1/arith/arith-int-009.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ; ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc index 4ac85a984..aa649ba4a 100644 --- a/test/regress/regress1/arith/arith-int-010.cvc +++ b/test/regress/regress1/arith/arith-int-010.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ; ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-011.cvc b/test/regress/regress1/arith/arith-int-011.cvc index bd2fa2a0d..7de68533f 100644 --- a/test/regress/regress1/arith/arith-int-011.cvc +++ b/test/regress/regress1/arith/arith-int-011.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ; ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9; diff --git a/test/regress/regress1/arith/arith-int-012.cvc b/test/regress/regress1/arith/arith-int-012.cvc index 11b0dab27..10922dd89 100644 --- a/test/regress/regress1/arith/arith-int-012.cvc +++ b/test/regress/regress1/arith/arith-int-012.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ; ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24; diff --git a/test/regress/regress1/arith/arith-int-013.cvc b/test/regress/regress1/arith/arith-int-013.cvc index 329251cae..8a1f76add 100644 --- a/test/regress/regress1/arith/arith-int-013.cvc +++ b/test/regress/regress1/arith/arith-int-013.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ; ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc index 6774dd2d1..951650461 100644 --- a/test/regress/regress1/arith/arith-int-016.cvc +++ b/test/regress/regress1/arith/arith-int-016.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ; ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc index e9a06125a..48287249f 100644 --- a/test/regress/regress1/arith/arith-int-017.cvc +++ b/test/regress/regress1/arith/arith-int-017.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ; ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc index 4cb97b77e..cae6fed72 100644 --- a/test/regress/regress1/arith/arith-int-018.cvc +++ b/test/regress/regress1/arith/arith-int-018.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ; ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc index cf9ae2d70..a26bbac01 100644 --- a/test/regress/regress1/arith/arith-int-019.cvc +++ b/test/regress/regress1/arith/arith-int-019.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ; ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc index 07a827465..c1416b38f 100644 --- a/test/regress/regress1/arith/arith-int-020.cvc +++ b/test/regress/regress1/arith/arith-int-020.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ; ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-022.cvc b/test/regress/regress1/arith/arith-int-022.cvc index 584348da4..4612f72c9 100644 --- a/test/regress/regress1/arith/arith-int-022.cvc +++ b/test/regress/regress1/arith/arith-int-022.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-024.cvc b/test/regress/regress1/arith/arith-int-024.cvc index f57136dd1..73ae7c4ad 100644 --- a/test/regress/regress1/arith/arith-int-024.cvc +++ b/test/regress/regress1/arith/arith-int-024.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc index 9e69aa2d1..52f2478e0 100644 --- a/test/regress/regress1/arith/arith-int-026.cvc +++ b/test/regress/regress1/arith/arith-int-026.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ; ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc index b45622fea..6c38642d2 100644 --- a/test/regress/regress1/arith/arith-int-027.cvc +++ b/test/regress/regress1/arith/arith-int-027.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ; ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc index 61fee4203..7e8b78893 100644 --- a/test/regress/regress1/arith/arith-int-028.cvc +++ b/test/regress/regress1/arith/arith-int-028.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ; ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc index ee49bbb68..ba49219d8 100644 --- a/test/regress/regress1/arith/arith-int-029.cvc +++ b/test/regress/regress1/arith/arith-int-029.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ; ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc index 70b6a3785..a6348b107 100644 --- a/test/regress/regress1/arith/arith-int-030.cvc +++ b/test/regress/regress1/arith/arith-int-030.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ; ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc index 86242f7aa..056ab622e 100644 --- a/test/regress/regress1/arith/arith-int-031.cvc +++ b/test/regress/regress1/arith/arith-int-031.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ; ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc index 1ee4c9844..08c29108e 100644 --- a/test/regress/regress1/arith/arith-int-032.cvc +++ b/test/regress/regress1/arith/arith-int-032.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ; ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc index 599ba4e9a..8259a7725 100644 --- a/test/regress/regress1/arith/arith-int-033.cvc +++ b/test/regress/regress1/arith/arith-int-033.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ; ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc index ec615a785..2b5ae4f4f 100644 --- a/test/regress/regress1/arith/arith-int-034.cvc +++ b/test/regress/regress1/arith/arith-int-034.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ; ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc index e7dee2484..1bad259e2 100644 --- a/test/regress/regress1/arith/arith-int-035.cvc +++ b/test/regress/regress1/arith/arith-int-035.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ; ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc index 9594f9586..0eb783815 100644 --- a/test/regress/regress1/arith/arith-int-036.cvc +++ b/test/regress/regress1/arith/arith-int-036.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ; ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc index 4d4422d3f..c3ed60011 100644 --- a/test/regress/regress1/arith/arith-int-037.cvc +++ b/test/regress/regress1/arith/arith-int-037.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ; ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc index 476133b24..52ac2b1e3 100644 --- a/test/regress/regress1/arith/arith-int-038.cvc +++ b/test/regress/regress1/arith/arith-int-038.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ; ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc index 9e9235ae8..cecb7f085 100644 --- a/test/regress/regress1/arith/arith-int-039.cvc +++ b/test/regress/regress1/arith/arith-int-039.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ; ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc index 68502349f..f2dff7796 100644 --- a/test/regress/regress1/arith/arith-int-040.cvc +++ b/test/regress/regress1/arith/arith-int-040.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ; ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc index a0c2dc0f9..9df03a9bd 100644 --- a/test/regress/regress1/arith/arith-int-041.cvc +++ b/test/regress/regress1/arith/arith-int-041.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ; ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc index 7efea85e5..7a2d6d6af 100644 --- a/test/regress/regress1/arith/arith-int-043.cvc +++ b/test/regress/regress1/arith/arith-int-043.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ; ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc index f933b014b..649532a4b 100644 --- a/test/regress/regress1/arith/arith-int-044.cvc +++ b/test/regress/regress1/arith/arith-int-044.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed %%%% down from 24, up from 6, up from 39 x0, x1, x2, x3 : INT; ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc index ca1a12ba6..2c552c915 100644 --- a/test/regress/regress1/arith/arith-int-045.cvc +++ b/test/regress/regress1/arith/arith-int-045.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ; ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc index d4d206c6e..acf4dc9a9 100644 --- a/test/regress/regress1/arith/arith-int-046.cvc +++ b/test/regress/regress1/arith/arith-int-046.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ; ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ; diff --git a/test/regress/regress1/arith/arith-int-047.cvc b/test/regress/regress1/arith/arith-int-047.cvc index 0763e5dc3..bb1225b9d 100644 --- a/test/regress/regress1/arith/arith-int-047.cvc +++ b/test/regress/regress1/arith/arith-int-047.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10; ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ; diff --git a/test/regress/regress1/arith/arith-int-048.cvc b/test/regress/regress1/arith/arith-int-048.cvc index e7c05332d..ccc84f389 100644 --- a/test/regress/regress1/arith/arith-int-048.cvc +++ b/test/regress/regress1/arith/arith-int-048.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ; ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc index 8eabc78a8..72e3b7f31 100644 --- a/test/regress/regress1/arith/arith-int-049.cvc +++ b/test/regress/regress1/arith/arith-int-049.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ; ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ; diff --git a/test/regress/regress1/arith/arith-int-050.cvc b/test/regress/regress1/arith/arith-int-050.cvc index f0ba939b7..21dbfe09a 100644 --- a/test/regress/regress1/arith/arith-int-050.cvc +++ b/test/regress/regress1/arith/arith-int-050.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ; ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc index 9a2497432..68654a7df 100644 --- a/test/regress/regress1/arith/arith-int-051.cvc +++ b/test/regress/regress1/arith/arith-int-051.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ; ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc index 83fdc89c8..9c9433ede 100644 --- a/test/regress/regress1/arith/arith-int-052.cvc +++ b/test/regress/regress1/arith/arith-int-052.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ; ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc index fa38fa3da..544d53fb9 100644 --- a/test/regress/regress1/arith/arith-int-053.cvc +++ b/test/regress/regress1/arith/arith-int-053.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ; ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc index 9b0066966..5b4181a11 100644 --- a/test/regress/regress1/arith/arith-int-054.cvc +++ b/test/regress/regress1/arith/arith-int-054.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ; ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc index 9729fb565..fdfa45848 100644 --- a/test/regress/regress1/arith/arith-int-055.cvc +++ b/test/regress/regress1/arith/arith-int-055.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ; ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc index e1c3ee1da..394b3dd4e 100644 --- a/test/regress/regress1/arith/arith-int-056.cvc +++ b/test/regress/regress1/arith/arith-int-056.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ; ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc index 4e7b939b4..252601514 100644 --- a/test/regress/regress1/arith/arith-int-057.cvc +++ b/test/regress/regress1/arith/arith-int-057.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ; ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc index 4d964f1c6..7e2a04d45 100644 --- a/test/regress/regress1/arith/arith-int-058.cvc +++ b/test/regress/regress1/arith/arith-int-058.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ; ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc index 841d9c8e1..87773679e 100644 --- a/test/regress/regress1/arith/arith-int-059.cvc +++ b/test/regress/regress1/arith/arith-int-059.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ; ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc index 227cb49b1..74dd16dca 100644 --- a/test/regress/regress1/arith/arith-int-060.cvc +++ b/test/regress/regress1/arith/arith-int-060.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ; ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc index 4a3cc28d0..b3bd247b2 100644 --- a/test/regress/regress1/arith/arith-int-061.cvc +++ b/test/regress/regress1/arith/arith-int-061.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ; ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc index f9a3156a2..0a185eb68 100644 --- a/test/regress/regress1/arith/arith-int-062.cvc +++ b/test/regress/regress1/arith/arith-int-062.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ; ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc index d88104688..13c4aae2e 100644 --- a/test/regress/regress1/arith/arith-int-063.cvc +++ b/test/regress/regress1/arith/arith-int-063.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ; ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc index 21ca822e1..f50b3cd97 100644 --- a/test/regress/regress1/arith/arith-int-064.cvc +++ b/test/regress/regress1/arith/arith-int-064.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ; ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc index b1b9e1b51..354eb981c 100644 --- a/test/regress/regress1/arith/arith-int-065.cvc +++ b/test/regress/regress1/arith/arith-int-065.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ; ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc index 9532b4198..f53a254bd 100644 --- a/test/regress/regress1/arith/arith-int-066.cvc +++ b/test/regress/regress1/arith/arith-int-066.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ; ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc index 5d7b52e69..61159e9aa 100644 --- a/test/regress/regress1/arith/arith-int-067.cvc +++ b/test/regress/regress1/arith/arith-int-067.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ; ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc index 107a21a12..683d36801 100644 --- a/test/regress/regress1/arith/arith-int-068.cvc +++ b/test/regress/regress1/arith/arith-int-068.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ; ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc index 3fab229b0..356a28013 100644 --- a/test/regress/regress1/arith/arith-int-069.cvc +++ b/test/regress/regress1/arith/arith-int-069.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ; ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc index cd828da5f..791b3b8af 100644 --- a/test/regress/regress1/arith/arith-int-070.cvc +++ b/test/regress/regress1/arith/arith-int-070.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ; ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc index ce5336476..d44b18b45 100644 --- a/test/regress/regress1/arith/arith-int-071.cvc +++ b/test/regress/regress1/arith/arith-int-071.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ; ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc index 10222deae..fb13a6616 100644 --- a/test/regress/regress1/arith/arith-int-072.cvc +++ b/test/regress/regress1/arith/arith-int-072.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ; ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc index 98e74be8f..784190cad 100644 --- a/test/regress/regress1/arith/arith-int-073.cvc +++ b/test/regress/regress1/arith/arith-int-073.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ; ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc index 28cc48186..914cbe8e3 100644 --- a/test/regress/regress1/arith/arith-int-074.cvc +++ b/test/regress/regress1/arith/arith-int-074.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ; ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc index 3b5131e8b..d3851e284 100644 --- a/test/regress/regress1/arith/arith-int-075.cvc +++ b/test/regress/regress1/arith/arith-int-075.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ; ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc index 2c8de7cdf..25a3a7d35 100644 --- a/test/regress/regress1/arith/arith-int-076.cvc +++ b/test/regress/regress1/arith/arith-int-076.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ; ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc index d14da386e..7e4482093 100644 --- a/test/regress/regress1/arith/arith-int-077.cvc +++ b/test/regress/regress1/arith/arith-int-077.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ; ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc index 3197c6524..eacccc375 100644 --- a/test/regress/regress1/arith/arith-int-078.cvc +++ b/test/regress/regress1/arith/arith-int-078.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ; ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc index 8be0f9a73..bf6b90c67 100644 --- a/test/regress/regress1/arith/arith-int-080.cvc +++ b/test/regress/regress1/arith/arith-int-080.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ; ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc index 546148376..47cc66ae2 100644 --- a/test/regress/regress1/arith/arith-int-081.cvc +++ b/test/regress/regress1/arith/arith-int-081.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8; ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc index 62bd45de7..a6245f036 100644 --- a/test/regress/regress1/arith/arith-int-082.cvc +++ b/test/regress/regress1/arith/arith-int-082.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ; ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc index 6b1084353..3a7c635cc 100644 --- a/test/regress/regress1/arith/arith-int-083.cvc +++ b/test/regress/regress1/arith/arith-int-083.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ; ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ; diff --git a/test/regress/regress1/arith/arith-int-084.cvc b/test/regress/regress1/arith/arith-int-084.cvc index 5f0e17afe..d4a0a966c 100644 --- a/test/regress/regress1/arith/arith-int-084.cvc +++ b/test/regress/regress1/arith/arith-int-084.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ; ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ; diff --git a/test/regress/regress1/arith/arith-int-085.cvc b/test/regress/regress1/arith/arith-int-085.cvc index 74dd714e8..b1a343e73 100644 --- a/test/regress/regress1/arith/arith-int-085.cvc +++ b/test/regress/regress1/arith/arith-int-085.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed %% down from 3 x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc index 64c212b3c..6ee96589b 100644 --- a/test/regress/regress1/arith/arith-int-086.cvc +++ b/test/regress/regress1/arith/arith-int-086.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ; ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc index 312c08917..b969df1a3 100644 --- a/test/regress/regress1/arith/arith-int-087.cvc +++ b/test/regress/regress1/arith/arith-int-087.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ; ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc index 5212640be..de0d23844 100644 --- a/test/regress/regress1/arith/arith-int-088.cvc +++ b/test/regress/regress1/arith/arith-int-088.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ; ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc index 7ff36d29e..e50daa9de 100644 --- a/test/regress/regress1/arith/arith-int-089.cvc +++ b/test/regress/regress1/arith/arith-int-089.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ; ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc index 52b9c13f0..74d4ba4db 100644 --- a/test/regress/regress1/arith/arith-int-090.cvc +++ b/test/regress/regress1/arith/arith-int-090.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ; ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc index 29a19db39..c03b544a3 100644 --- a/test/regress/regress1/arith/arith-int-091.cvc +++ b/test/regress/regress1/arith/arith-int-091.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ; ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc index 51c8a6bc4..d080cde0c 100644 --- a/test/regress/regress1/arith/arith-int-092.cvc +++ b/test/regress/regress1/arith/arith-int-092.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ; ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc index 7d2123d41..e910def47 100644 --- a/test/regress/regress1/arith/arith-int-093.cvc +++ b/test/regress/regress1/arith/arith-int-093.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ; ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc index a5f1aefce..2204bba4e 100644 --- a/test/regress/regress1/arith/arith-int-094.cvc +++ b/test/regress/regress1/arith/arith-int-094.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ; ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc index bc47d6f49..e803dbe9b 100644 --- a/test/regress/regress1/arith/arith-int-095.cvc +++ b/test/regress/regress1/arith/arith-int-095.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ; ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc index 2f6cf3155..354ae180d 100644 --- a/test/regress/regress1/arith/arith-int-096.cvc +++ b/test/regress/regress1/arith/arith-int-096.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ; ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28; diff --git a/test/regress/regress1/arith/arith-int-097.cvc b/test/regress/regress1/arith/arith-int-097.cvc index b05061192..67eb614eb 100644 --- a/test/regress/regress1/arith/arith-int-097.cvc +++ b/test/regress/regress1/arith/arith-int-097.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ; ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc index 0d74dcb39..57a45de03 100644 --- a/test/regress/regress1/arith/arith-int-099.cvc +++ b/test/regress/regress1/arith/arith-int-099.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ; ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc index 7e07bee14..66be1f8f7 100644 --- a/test/regress/regress1/arith/arith-int-100.cvc +++ b/test/regress/regress1/arith/arith-int-100.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ; ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ; diff --git a/test/regress/regress1/boolean.cvc b/test/regress/regress1/boolean.cvc index eb0e7ab52..2c861c0f0 100644 --- a/test/regress/regress1/boolean.cvc +++ b/test/regress/regress1/boolean.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed p : BOOLEAN; q : BOOLEAN; r : BOOLEAN; diff --git a/test/regress/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc index eebcbc2f8..5306a1513 100644 --- a/test/regress/regress1/fmf/ko-bound-set.cvc +++ b/test/regress/regress1/fmf/ko-bound-set.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; OPTION "produce-models"; diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc index dfa9b72d5..5ec31d801 100644 --- a/test/regress/regress1/hole6.cvc +++ b/test/regress/regress1/hole6.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc index f7407a2a5..6f2a8764b 100644 --- a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc +++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; diff --git a/test/regress/regress1/test12.cvc b/test/regress/regress1/test12.cvc index 37687bee1..39ced0428 100644 --- a/test/regress/regress1/test12.cvc +++ b/test/regress/regress1/test12.cvc @@ -1,34 +1,34 @@ % COMMAND-LINE: --incremental -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: valid -% EXPECT: valid +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: entailed +% EXPECT: entailed A: TYPE; P_1: BOOLEAN; P_2: BOOLEAN; diff --git a/test/regress/regress2/arith/arith-int-098.cvc b/test/regress/regress2/arith/arith-int-098.cvc index 08cfd9c9c..cf20f2b61 100644 --- a/test/regress/regress2/arith/arith-int-098.cvc +++ b/test/regress/regress2/arith/arith-int-098.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ; ASSERT (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12; diff --git a/test/regress/regress2/hole7.cvc b/test/regress/regress2/hole7.cvc index 1f762477a..e73588bad 100644 --- a/test/regress/regress2/hole7.cvc +++ b/test/regress/regress2/hole7.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/hole8.cvc b/test/regress/regress2/hole8.cvc index 705c95ea6..a46c4da97 100644 --- a/test/regress/regress2/hole8.cvc +++ b/test/regress/regress2/hole8.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/typed_v1l50016-simp.cvc b/test/regress/regress2/typed_v1l50016-simp.cvc index b4a1e4b32..1d576ab74 100644 --- a/test/regress/regress2/typed_v1l50016-simp.cvc +++ b/test/regress/regress2/typed_v1l50016-simp.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress3/hole9.cvc b/test/regress/regress3/hole9.cvc index e60839f7b..b86b3b039 100644 --- a/test/regress/regress3/hole9.cvc +++ b/test/regress/regress3/hole9.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress4/hole10.cvc b/test/regress/regress4/hole10.cvc index ebc8279d3..fb4c41b35 100644 --- a/test/regress/regress4/hole10.cvc +++ b/test/regress/regress4/hole10.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index 141db4eea..2ce50949b 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -29,8 +29,8 @@ int main() { ExprManager em; Options opts; SmtEngine smt(&em); - Result r = smt.query(em.mkConst(true)); + Result r = smt.checkEntailed(em.mkConst(true)); - return (Result::VALID == r) ? 0 : 1; + return (Result::ENTAILED == r) ? 0 : 1; } diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index fb9714d4b..2924359e8 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -35,9 +35,10 @@ int main() { Expr y = em.mkVar("y", em.integerType()); smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5)))); Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0))); - Result r = smt.query(q); + Result r = smt.checkEntailed(q); - if(r != Result::INVALID) { + if (r != Result::NOT_ENTAILED) + { exit(1); } @@ -47,7 +48,7 @@ int main() { } smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5)))); - r = smt.query(q); + r = smt.checkEntailed(q); Statistics stats2 = smt.getStatistics(); bool different = false; for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) { @@ -68,5 +69,5 @@ int main() { } #endif /* CVC4_STATISTICS_ON */ - return r == Result::VALID ? 0 : 1; + return r == Result::ENTAILED ? 0 : 1; } diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp index a7266e0b0..8698fde0e 100644 --- a/test/system/two_smt_engines.cpp +++ b/test/system/two_smt_engines.cpp @@ -28,9 +28,9 @@ int main() { Options opts; SmtEngine smt(&em); SmtEngine smt2(&em); - Result r = smt.query(em.mkConst(true)); - Result r2 = smt2.query(em.mkConst(true)); + Result r = smt.checkEntailed(em.mkConst(true)); + Result r2 = smt2.checkEntailed(em.mkConst(true)); - return r == Result::VALID && r2 == Result::VALID ? 0 : 1; + return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1; } diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h index ab5d65e72..cbfc9cf23 100644 --- a/test/unit/api/result_black.h +++ b/test/unit/api/result_black.h @@ -29,9 +29,8 @@ class ResultBlack : public CxxTest::TestSuite void testIsSat(); void testIsUnsat(); void testIsSatUnknown(); - void testIsValid(); - void testIsInvalid(); - void testIsValidUnknown(); + void testIsEntailed(); + void testIsEntailmentUnknown(); private: std::unique_ptr<Solver> d_solver; @@ -44,9 +43,9 @@ void ResultBlack::testIsNull() TS_ASSERT(!res_null.isSat()); TS_ASSERT(!res_null.isUnsat()); TS_ASSERT(!res_null.isSatUnknown()); - TS_ASSERT(!res_null.isValid()); - TS_ASSERT(!res_null.isInvalid()); - TS_ASSERT(!res_null.isValidUnknown()); + TS_ASSERT(!res_null.isEntailed()); + TS_ASSERT(!res_null.isNotEntailed()); + TS_ASSERT(!res_null.isEntailmentUnknown()); Sort u_sort = d_solver->mkUninterpretedSort("u"); Term x = d_solver->mkVar(u_sort, "x"); d_solver->assertFormula(x.eqTerm(x)); @@ -100,27 +99,24 @@ void ResultBlack::testIsSatUnknown() TS_ASSERT(res.isSatUnknown()); } -void ResultBlack::testIsValid() +void ResultBlack::testIsEntailed() { + d_solver->setOption("incremental", "true"); Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkValid(); - TS_ASSERT(res.isValid()); - TS_ASSERT(!res.isValidUnknown()); -} - -void ResultBlack::testIsInvalid() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkValid(); - TS_ASSERT(res.isInvalid()); - TS_ASSERT(!res.isValidUnknown()); + Term x = d_solver->mkConst(u_sort, "x"); + Term y = d_solver->mkConst(u_sort, "y"); + Term a = x.eqTerm(y).notTerm(); + Term b = x.eqTerm(y); + d_solver->assertFormula(a); + Result entailed = d_solver->checkEntailed(a); + TS_ASSERT(entailed.isEntailed()); + TS_ASSERT(!entailed.isEntailmentUnknown()); + Result not_entailed = d_solver->checkEntailed(b); + TS_ASSERT(not_entailed.isNotEntailed()); + TS_ASSERT(!not_entailed.isEntailmentUnknown()); } -void ResultBlack::testIsValidUnknown() +void ResultBlack::testIsEntailmentUnknown() { d_solver->setLogic("QF_NIA"); d_solver->setOption("incremental", "false"); @@ -128,9 +124,9 @@ void ResultBlack::testIsValidUnknown() Sort int_sort = d_solver->getIntegerSort(); Term x = d_solver->mkVar(int_sort, "x"); d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkValid(); - TS_ASSERT(!res.isValid()); - TS_ASSERT(res.isValidUnknown()); + Result res = d_solver->checkEntailed(x.eqTerm(x)); + TS_ASSERT(!res.isEntailed()); + TS_ASSERT(res.isEntailmentUnknown()); TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); } diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 0eefde700..9fd1b7789 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -95,10 +95,9 @@ class SolverBlack : public CxxTest::TestSuite void testPop3(); void testSimplify(); - void testCheckValid1(); - void testCheckValid2(); - void testCheckValidAssuming1(); - void testCheckValidAssuming2(); + void testCheckEntailed(); + void testCheckEntailed1(); + void testCheckEntailed2(); void testSetInfo(); void testSetLogic(); @@ -1104,51 +1103,28 @@ void SolverBlack::testSimplify() TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2)); } -void SolverBlack::testCheckValid1() +void SolverBlack::testCheckEntailed() { d_solver->setOption("incremental", "false"); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); - TS_ASSERT_THROWS(d_solver->checkValid(), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()), + CVC4ApiException&); } -void SolverBlack::testCheckValid2() +void SolverBlack::testCheckEntailed1() { + Sort boolSort = d_solver->getBooleanSort(); + Term x = d_solver->mkConst(boolSort, "x"); + Term y = d_solver->mkConst(boolSort, "y"); + Term z = d_solver->mkTerm(AND, x, y); d_solver->setOption("incremental", "true"); - - Sort realSort = d_solver->getRealSort(); - Sort intSort = d_solver->getIntegerSort(); - - // Constants - Term x = d_solver->mkConst(intSort, "x"); - Term y = d_solver->mkConst(realSort, "y"); - // Values - Term three = d_solver->mkReal(3); - Term neg2 = d_solver->mkReal(-2); - Term two_thirds = d_solver->mkReal(2, 3); - // Terms - Term three_y = d_solver->mkTerm(MULT, three, y); - Term diff = d_solver->mkTerm(MINUS, y, x); - // Formulas - Term x_geq_3y = d_solver->mkTerm(GEQ, x, three_y); - Term x_leq_y = d_solver->mkTerm(LEQ, x, y); - Term neg2_lt_x = d_solver->mkTerm(LT, neg2, x); - // Assertions - Term assertions = d_solver->mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); - - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); - d_solver->assertFormula(assertions); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValid()); -} - -void SolverBlack::testCheckValidAssuming1() -{ - d_solver->setOption("incremental", "false"); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue())); - TS_ASSERT_THROWS(d_solver->checkValidAssuming(d_solver->mkTrue()), - CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z)); } -void SolverBlack::testCheckValidAssuming2() +void SolverBlack::testCheckEntailed2() { d_solver->setOption("incremental", "true"); @@ -1185,15 +1161,15 @@ void SolverBlack::testCheckValidAssuming2() p_f_y // p(f(y)) }); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming(d_solver->mkTrue())); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue())); d_solver->assertFormula(assertions); TS_ASSERT_THROWS_NOTHING( - d_solver->checkValidAssuming(d_solver->mkTerm(DISTINCT, x, y))); - TS_ASSERT_THROWS_NOTHING(d_solver->checkValidAssuming( + d_solver->checkEntailed(d_solver->mkTerm(DISTINCT, x, y))); + TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed( {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)})); - TS_ASSERT_THROWS(d_solver->checkValidAssuming(n), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->checkEntailed(n), CVC4ApiException&); TS_ASSERT_THROWS( - d_solver->checkValidAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}), + d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}), CVC4ApiException&); } |