assign expected-status to regressions

diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index ac9885703822e218590ffb43b4ce75bdf0129407..89afbe325e9104895540161897cf7b90a72d73c9 100644 (file)
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 1
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% EXPECT: VALID
 p : BOOLEAN;
 q : BOOLEAN;
 r : BOOLEAN;

diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc
index d2c24a4380d6fee2addd02b7291f4d10ca2120a7..d3d936381b8b8144efd4782c5301f91717eef039 100644 (file)
--- a/test/regress/regress0/bug1.cvc
+++ b/test/regress/regress0/bug1.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 0
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% EXPECT: VALID
 x : REAL;
 y : REAL;
 f : REAL -> REAL;

diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index 28738fc24f310860ab515706545bc1384e21b078..bdd45b6d0499c5e7058f3812ea188cb74310e1d5 100644 (file)
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 0
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% EXPECT: VALID
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;

diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc
index 0cb00599d6b942c48beb0ff5516cdaa8bcebaee4..7bd2a356d82ff74943507be64f89ebec8a1681fe 100644 (file)
--- a/test/regress/regress0/logops.cvc
+++ b/test/regress/regress0/logops.cvc
@@ -1,14 +1,17 @@
-
-
 a, b, c: BOOLEAN;
 
+% EXPECT: VALID
 QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
 
+% EXPECT: INVALID
 QUERY NOT c AND b;
 
+% EXPECT: VALID
 QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
 
+% EXPECT: VALID
 QUERY (a => b) <=> (NOT a OR b);
 
+% EXPECT: VALID
 QUERY TRUE XOR FALSE;
  

diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc
index 8f7ceedd553ebba96f6b98185485a6e2fd09559f..36107e784844fb10a177120fded0096d3724fa35 100644 (file)
--- a/test/regress/regress0/queries0.cvc
+++ b/test/regress/regress0/queries0.cvc
@@ -1,11 +1,10 @@
-
 % Tests the invariants for multiple queries.
 
 a, b: BOOLEAN;
 
-%Valid query
+% EXPECT: VALID
 QUERY (a AND b) OR NOT (a AND b);
 
-%Invalid query
+% EXPECT: INVALID
 QUERY (a OR b);
 

diff --git a/test/regress/regress0/simple-uf.smt b/test/regress/regress0/simple-uf.smt
index 3aaba2ab088082ae12287ba6ccf1b5d942e9627e..9611a6d799aede40e3d0562f71194885b9be12c7 100644 (file)
--- a/test/regress/regress0/simple-uf.smt
+++ b/test/regress/regress0/simple-uf.smt
@@ -1,5 +1,6 @@
 (benchmark simple_uf
   :logic QF_UF
+  :status unsat
   :extrasorts (A B)
   :extrafuns ((f A B) (x A) (y A))
   :formula (not (implies (= x y) (= (f x) (f y))))

diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc
index 3566053d9d91442d22b623bf3ef54b9291a03645..21145b6e0e95cecf7c4878f61665125f5d1148ef 100644 (file)
--- a/test/regress/regress0/simple.cvc
+++ b/test/regress/regress0/simple.cvc
@@ -3,4 +3,5 @@ ASSERT x1 OR NOT x0;
 ASSERT x0 OR NOT x3;
 ASSERT x3 OR x2;
 ASSERT x1 AND NOT x1;
+% EXPECT: VALID
 QUERY x2;

diff --git a/test/regress/regress0/simple.smt b/test/regress/regress0/simple.smt
index 56aa82d721b263486ea1011ed69e8f6a48005eba..2c1cf7ce70fd911d763d86af60d041c80d2e664a 100644 (file)
--- a/test/regress/regress0/simple.smt
+++ b/test/regress/regress0/simple.smt
@@ -1,5 +1,5 @@
 (benchmark b
-:status unknown
+:status unsat
 :logic QF_UF
 :extrapreds ((x0))
 :extrapreds ((x1))

diff --git a/test/regress/regress0/simple2.smt b/test/regress/regress0/simple2.smt
index e917d1b64c2f103a0b706cd47a2665917dd7e137..3d523b3c37cdacc075d5d5b5065f70619d9f7652 100644 (file)
--- a/test/regress/regress0/simple2.smt
+++ b/test/regress/regress0/simple2.smt
@@ -1,5 +1,5 @@
 (benchmark b
-:status unknown
+:status sat
 :logic QF_UF
 :extrapreds ((x0))
 :extrapreds ((x1))

diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc
index 3ad6f124a796afedce342c886c19ae1406f0e1c9..3a36b8c1e0956af63c52bbee8df6b36b8aa12539 100644 (file)
--- a/test/regress/regress0/smallcnf.cvc
+++ b/test/regress/regress0/smallcnf.cvc
@@ -1,9 +1,9 @@
-
 a, b, c : BOOLEAN;
 
 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
 QUERY FALSE;
 

diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc
index ff0880b2a8dabc0792d74549ee090c2d3b6b4f80..6f0cac8fa4aae40fd5d7394ba21f57144f23f88f 100644 (file)
--- a/test/regress/regress0/test11.cvc
+++ b/test/regress/regress0/test11.cvc
@@ -1,11 +1,7 @@
-%% Regression level = 0
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
-
 x, y : BOOLEAN;
 
 ASSERT (x OR y);
 ASSERT NOT (x OR y);
 
+% EXPECT: VALID
 QUERY FALSE;

diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc
index 31ec0864ebd0e578b7ff8f8e8c5f4b90933058e8..48966f53b2e0f1e950c729a687af8cc457e69aab 100644 (file)
--- a/test/regress/regress0/test12.cvc
+++ b/test/regress/regress0/test12.cvc
@@ -1,7 +1,33 @@
-%% Regression level = 1
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% 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 eabbc97740623ad7c9a94a7881d826cb772e54bf..de6be2f545d17d8da450ead182dae5b57fb1bb6b 100644 (file)
--- a/test/regress/regress0/test9.cvc
+++ b/test/regress/regress0/test9.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 0
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% EXPECT: VALID
 P,Q:BOOLEAN;
 ASSERT (P OR Q);
 QUERY (P OR Q);

diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc
index 5e7b22b6446e1e003445da4748a24eec61041d47..74fdb11165c21779d8885f5e70c7db3287aa13d1 100644 (file)
--- a/test/regress/regress0/uf20-03.cvc
+++ b/test/regress/regress0/uf20-03.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 0
-%% Result = Invalid
-%% Runtime = 1
-%% Language = presentation
+% EXPECT: INVALID
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;

diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc
index ab888039e09d8700553d10d860620c0606a231c6..b5894dbad3c63df9493eb399225b52146107d32a 100644 (file)
--- a/test/regress/regress0/wiki.cvc
+++ b/test/regress/regress0/wiki.cvc
@@ -1,4 +1,24 @@
-
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
+% EXPECT: VALID
 
 a, b, c : BOOLEAN;
 

diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc
index 0ab9c798ef230c871980eb175c162b925a235378..1bebf80497dd43df5bd48a3a3a69aed2ab179c9c 100644 (file)
--- a/test/regress/regress1/hole7.cvc
+++ b/test/regress/regress1/hole7.cvc
@@ -1,8 +1,4 @@
-%% Regression level = 1
-%% Result = Valid
-%% Runtime = 1
-%% Up from 2 (actual 2.1sec), Down from 4
-%% Language = presentation
+% 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 d5fe5897ab2d01de4e494b4fbcae857e17945e44..65942a27fdca918fc832112a775897e22d237d5b 100644 (file)
--- a/test/regress/regress1/hole8.cvc
+++ b/test/regress/regress1/hole8.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 1
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% 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 e6a0d420b182fffd2b7d6280ddbb2d8eab40c3fe..93377ca0b7195effffabbb436ec24ca3986c0b5d 100644 (file)
--- a/test/regress/regress2/hole9.cvc
+++ b/test/regress/regress2/hole9.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 1
-%% Result = Valid
-%% Runtime = 1
-%% Language = presentation
+% 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 22adeda676131688d46164dd20aab918e05c01c7..39c978b189b8326a9d8e9eac278b7f353a9532cb 100644 (file)
--- a/test/regress/regress3/hole10.cvc
+++ b/test/regress/regress3/hole10.cvc
@@ -1,7 +1,4 @@
-%% Regression level = 2
-%% Result = Valid
-%% Runtime = 2
-%% Language = presentation
+% EXPECT: VALID
 x_1 : BOOLEAN;
 x_2 : BOOLEAN;
 x_3 : BOOLEAN;