assign expected-status to regressions

19 files changed, 73 insertions, 55 deletions

diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index ac9885703..89afbe325 100644
--- 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 d2c24a438..d3d936381 100644
--- 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 28738fc24..bdd45b6d0 100644
--- 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 0cb00599d..7bd2a356d 100644
--- 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 8f7ceedd5..36107e784 100644
--- 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 3aaba2ab0..9611a6d79 100644
--- 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 3566053d9..21145b6e0 100644
--- 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 56aa82d72..2c1cf7ce7 100644
--- 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 e917d1b64..3d523b3c3 100644
--- 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 3ad6f124a..3a36b8c1e 100644
--- 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 ff0880b2a..6f0cac8fa 100644
--- 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 31ec0864e..48966f53b 100644
--- 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 eabbc9774..de6be2f54 100644
--- 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 5e7b22b64..74fdb1116 100644
--- 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 ab888039e..b5894dbad 100644
--- 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 0ab9c798e..1bebf8049 100644
--- 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 d5fe5897a..65942a27f 100644
--- 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 e6a0d420b..93377ca0b 100644
--- 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 22adeda67..39c978b18 100644
--- 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;