diff options
Diffstat (limited to 'test/regress')
69 files changed, 102 insertions, 102 deletions
diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc index 5b4a33bed..d153464e1 100644 --- a/test/regress/regress0/arith/arith.01.cvc +++ b/test/regress/regress0/arith/arith.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc index a2c93da46..76a7a4338 100644 --- a/test/regress/regress0/arith/arith.02.cvc +++ b/test/regress/regress0/arith/arith.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid 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 96af458f0..007adf1d6 100644 --- a/test/regress/regress0/arith/arith.03.cvc +++ b/test/regress/regress0/arith/arith.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x : REAL; y : REAL; diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index d0205116c..cdfb3a09f 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index eeac40c9f..fe3450c27 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid p : BOOLEAN; q : BOOLEAN; r : BOOLEAN; diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index c6d79a4ab..394f89e51 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid a:BOOLEAN; b:BOOLEAN; ASSERT(a); diff --git a/test/regress/regress0/cvc3-bug15.cvc b/test/regress/regress0/cvc3-bug15.cvc index aaebeebd6..371374078 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: valid x : REAL; y : REAL; f : REAL -> REAL; diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 07bfa392c..64231aaf5 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress0/ite.cvc b/test/regress/regress0/ite.cvc index 0a3e7535a..5094c997d 100644 --- a/test/regress/regress0/ite.cvc +++ b/test/regress/regress0/ite.cvc @@ -1,4 +1,4 @@ -% EXPECT: UNSAT +% EXPECT: unsat % EXIT: 20 x, y : REAL; CHECKSAT (NOT (x = IF TRUE THEN x ELSE y ENDIF)); diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index 5348cf7e4..9a247d2c6 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); % EXIT: 20 diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index 4a8539fae..105cc7685 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: INVALID +% EXPECT: invalid QUERY NOT c AND b; % EXIT: 10 diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 6b5f34613..65126699c 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); % EXIT: 20 diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index 6e7aa1f5e..258307e8c 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,4 +1,4 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a => b) <=> (NOT a OR b); % EXIT: 20 diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 14e2c887a..b7308870e 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -1,5 +1,5 @@ a, b, c: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY TRUE XOR FALSE; % EXIT: 20 diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index 0de37db83..547633bf1 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 7b29bb95e..dfc03bf22 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 ef1345cc1..d19ab9aae 100644 --- a/test/regress/regress0/precedence/bool-cmp.cvc +++ b/test/regress/regress0/precedence/bool-cmp.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 af2823fcf..aff12548f 100644 --- a/test/regress/regress0/precedence/cmp-plus.cvc +++ b/test/regress/regress0/precedence/cmp-plus.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 e85b4a3e6..f207071b3 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 b92354753..a496ccf16 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 0115fc319..ee2e2479f 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 d465df313..b87038a99 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 f8c813ceb..4a2aa18a8 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 24edb4ecd..266daae40 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 8c849a0d9..048d971b4 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 6d712d43d..cf4a0e4a5 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 d91f79dc8..13f3a316e 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 47cc87c76..4e19be584 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 ecd34f583..9300ae6c4 100644 --- a/test/regress/regress0/precedence/plus-mult.cvc +++ b/test/regress/regress0/precedence/plus-mult.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 ba3f48a7f..950c8ee94 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 27911332c..a356f9b3a 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % 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 2b4436937..837e4c575 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid % Simple test for right precedence of OR and XOR. A, B, C: BOOLEAN; diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc index fe6235981..110984083 100644 --- a/test/regress/regress0/queries0.cvc +++ b/test/regress/regress0/queries0.cvc @@ -2,10 +2,10 @@ a, b: BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY (a AND b) OR NOT (a AND b); -% EXPECT: INVALID +% EXPECT: invalid QUERY (a OR b); % EXIT: 10 diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index a0bff6c5a..4a16dcbe3 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -3,6 +3,6 @@ ASSERT x1 OR NOT x0; ASSERT x0 OR NOT x3; ASSERT x3 OR x2; ASSERT x1 AND NOT x1; -% EXPECT: VALID +% EXPECT: valid QUERY x2; % EXIT: 20 diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index fe17e0b53..dc316a9fb 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -4,7 +4,7 @@ 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: invalid QUERY FALSE; % EXIT: 10 diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 2fa1e23ba..f777e517e 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -3,6 +3,6 @@ x, y : BOOLEAN; ASSERT (x OR y); ASSERT NOT (x OR y); -% EXPECT: VALID +% EXPECT: valid QUERY FALSE; % EXIT: 20 diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc index a3d63b497..25245f36a 100644 --- a/test/regress/regress0/test12.cvc +++ b/test/regress/regress0/test12.cvc @@ -1,33 +1,33 @@ -% 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: 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 A: TYPE; P_1: BOOLEAN; P_2: BOOLEAN; diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index 64c2011a4..0cf587bca 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid 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 84b8b8a8d..141cc11fb 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid 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 21d3e3cee..3a72ce71a 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid 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 476c6cd4a..e0079c826 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid 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 c9675588d..649accd21 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid A: TYPE; B: TYPE; x, y: A; diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index a44b028a2..1b35efd7d 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -1,4 +1,4 @@ -% EXPECT: INVALID +% EXPECT: invalid 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 7b6835469..3833bb85f 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (b OR c) <=> (a OR b) OR c; % EXIT: 20 diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index 9fd4f8fb7..a431f9b22 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (b AND c) <=> (a AND b) AND c; % EXIT: 20 diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 63c1029b4..65acbb438 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR b <=> b OR a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index 77fa0059b..bcd724c8d 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND b <=> b AND a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index cb7140bcc..9469a9902 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (a AND b) <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 6c69ca4bc..64663e459 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (a OR b) <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index a0281d04b..85de76be7 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); % EXIT: 20 diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index ddf0f328c..cedf3dba0 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); % EXIT: 20 diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index f97021910..ded0edd5a 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR NOT a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index da8a1a9c3..dd1e7031a 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND NOT a <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index 4d7c3c130..61e404338 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR a <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index c932892c8..b73b0357b 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND a <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 3ad4fd4ab..6ae844616 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR FALSE <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 454cf442c..228a5af4f 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND TRUE <=> a; % EXIT: 20 diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index 81a13f798..b78e2cb80 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a OR TRUE <=> TRUE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index bd13faf11..0282c59af 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY a AND FALSE <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index 48949f89f..5d3b7629b 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT FALSE <=> TRUE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 8959d34a6..a34ceeef8 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT TRUE <=> FALSE; % EXIT: 20 diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index 11366526b..38c557514 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT (a OR b) <=> NOT a AND NOT b; % EXIT: 20 diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 5ef534bb0..cd166f956 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT (a AND b) <=> NOT a OR NOT b; % EXIT: 20 diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index bcd7146fb..a8fbafbc1 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -1,5 +1,5 @@ a, b, c : BOOLEAN; -% EXPECT: VALID +% EXPECT: valid QUERY NOT NOT a <=> a; % EXIT: 20 diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc index 5ff290f62..150c39e38 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress1/hole7.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc index d0f974619..fb9206aa0 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress1/hole8.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc index e631444d3..e9bd543ef 100644 --- a/test/regress/regress2/hole9.cvc +++ b/test/regress/regress2/hole9.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc index 661e3ef4b..ba29355db 100644 --- a/test/regress/regress3/hole10.cvc +++ b/test/regress/regress3/hole10.cvc @@ -1,4 +1,4 @@ -% EXPECT: VALID +% EXPECT: valid x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/run_regression b/test/regress/run_regression index ebef82cf1..614f02f0f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -52,10 +52,10 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then - expected_output=SAT + expected_output=sat expected_exit_status=10 elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=UNSAT + expected_output=unsat expected_exit_status=20 else error "cannot determine status of \`$benchmark'" @@ -80,10 +80,10 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_output=SAT + expected_output=sat expected_exit_status=10 elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=UNSAT + expected_output=unsat expected_exit_status=20 else error "cannot determine status of \`$benchmark'" |