Moved regressions into various levels based on running time.

40 files changed, 34 insertions, 14 deletions

diff --git a/test/regress/logops.cvc b/test/regress/logops.cvc
deleted file mode 100644
index 35e080992..000000000
--- a/test/regress/logops.cvc
+++ /dev/null
@@ -1,14 +0,0 @@
-
-
-a, b, c: BOOLEAN;
-
-%% QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
-
-%% QUERY NOT c AND b;
-
-QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
-
-%% QUERY (a => b) <=> (NOT a OR b);
-
-%% QUERY TRUE XOR FALSE;
- 
diff --git a/test/regress/boolean.cvc b/test/regress/regress0/boolean.cvc
index ac9885703..ac9885703 100644
--- a/test/regress/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
diff --git a/test/regress/bug1.cvc b/test/regress/regress0/bug1.cvc
index d2c24a438..d2c24a438 100644
--- a/test/regress/bug1.cvc
+++ b/test/regress/regress0/bug1.cvc
diff --git a/test/regress/hole6.cvc b/test/regress/regress0/hole6.cvc
index 28738fc24..28738fc24 100644
--- a/test/regress/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc
new file mode 100644
index 000000000..0cb00599d
--- /dev/null
+++ b/test/regress/regress0/logops.cvc
@@ -0,0 +1,14 @@
+
+
+a, b, c: BOOLEAN;
+
+QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
+
+QUERY NOT c AND b;
+
+QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
+
+QUERY (a => b) <=> (NOT a OR b);
+
+QUERY TRUE XOR FALSE;
+ 
diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc
new file mode 100644
index 000000000..8f7ceedd5
--- /dev/null
+++ b/test/regress/regress0/queries0.cvc
@@ -0,0 +1,11 @@
+
+% Tests the invariants for multiple queries.
+
+a, b: BOOLEAN;
+
+%Valid query
+QUERY (a AND b) OR NOT (a AND b);
+
+%Invalid query
+QUERY (a OR b);
+
diff --git a/test/regress/simple-uf.smt b/test/regress/regress0/simple-uf.smt
index 3aaba2ab0..3aaba2ab0 100644
--- a/test/regress/simple-uf.smt
+++ b/test/regress/regress0/simple-uf.smt
diff --git a/test/regress/simple.cvc b/test/regress/regress0/simple.cvc
index 3566053d9..3566053d9 100644
--- a/test/regress/simple.cvc
+++ b/test/regress/regress0/simple.cvc
diff --git a/test/regress/simple.smt b/test/regress/regress0/simple.smt
index 56aa82d72..56aa82d72 100644
--- a/test/regress/simple.smt
+++ b/test/regress/regress0/simple.smt
diff --git a/test/regress/simple2.smt b/test/regress/regress0/simple2.smt
index e917d1b64..e917d1b64 100644
--- a/test/regress/simple2.smt
+++ b/test/regress/regress0/simple2.smt
diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc
new file mode 100644
index 000000000..3ad6f124a
--- /dev/null
+++ b/test/regress/regress0/smallcnf.cvc
@@ -0,0 +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;
+QUERY FALSE;
+
diff --git a/test/regress/test11.cvc b/test/regress/regress0/test11.cvc
index ff0880b2a..ff0880b2a 100644
--- a/test/regress/test11.cvc
+++ b/test/regress/regress0/test11.cvc
diff --git a/test/regress/test12.cvc b/test/regress/regress0/test12.cvc
index 31ec0864e..31ec0864e 100644
--- a/test/regress/test12.cvc
+++ b/test/regress/regress0/test12.cvc
diff --git a/test/regress/test9.cvc b/test/regress/regress0/test9.cvc
index eabbc9774..eabbc9774 100644
--- a/test/regress/test9.cvc
+++ b/test/regress/regress0/test9.cvc
diff --git a/test/regress/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc
index 5e7b22b64..5e7b22b64 100644
--- a/test/regress/uf20-03.cvc
+++ b/test/regress/regress0/uf20-03.cvc
diff --git a/test/regress/wiki.cvc b/test/regress/regress0/wiki.cvc
index ab888039e..ab888039e 100644
--- a/test/regress/wiki.cvc
+++ b/test/regress/regress0/wiki.cvc
diff --git a/test/regress/friedman_n4_i5.smt b/test/regress/regress1/friedman_n4_i5.smt
index ff5c75735..ff5c75735 100644
--- a/test/regress/friedman_n4_i5.smt
+++ b/test/regress/regress1/friedman_n4_i5.smt
diff --git a/test/regress/hole7.cvc b/test/regress/regress1/hole7.cvc
index 0ab9c798e..0ab9c798e 100644
--- a/test/regress/hole7.cvc
+++ b/test/regress/regress1/hole7.cvc
diff --git a/test/regress/hole8.cvc b/test/regress/regress1/hole8.cvc
index d5fe5897a..d5fe5897a 100644
--- a/test/regress/hole8.cvc
+++ b/test/regress/regress1/hole8.cvc
diff --git a/test/regress/instance_1444.smt b/test/regress/regress1/instance_1444.smt
index 1bed83467..1bed83467 100644
--- a/test/regress/instance_1444.smt
+++ b/test/regress/regress1/instance_1444.smt
diff --git a/test/regress/bmc-galileo-8.smt b/test/regress/regress2/bmc-galileo-8.smt
index dbdd2bf28..dbdd2bf28 100644
--- a/test/regress/bmc-galileo-8.smt
+++ b/test/regress/regress2/bmc-galileo-8.smt
diff --git a/test/regress/bmc-galileo-9.smt b/test/regress/regress2/bmc-galileo-9.smt
index c78e7a0f1..c78e7a0f1 100644
--- a/test/regress/bmc-galileo-9.smt
+++ b/test/regress/regress2/bmc-galileo-9.smt
diff --git a/test/regress/bmc-ibm-1.smt b/test/regress/regress2/bmc-ibm-1.smt
index 9c210e3a1..9c210e3a1 100644
--- a/test/regress/bmc-ibm-1.smt
+++ b/test/regress/regress2/bmc-ibm-1.smt
diff --git a/test/regress/bmc-ibm-10.smt b/test/regress/regress2/bmc-ibm-10.smt
index acb0a9070..acb0a9070 100644
--- a/test/regress/bmc-ibm-10.smt
+++ b/test/regress/regress2/bmc-ibm-10.smt
diff --git a/test/regress/bmc-ibm-11.smt b/test/regress/regress2/bmc-ibm-11.smt
index 284761962..284761962 100644
--- a/test/regress/bmc-ibm-11.smt
+++ b/test/regress/regress2/bmc-ibm-11.smt
diff --git a/test/regress/bmc-ibm-12.smt b/test/regress/regress2/bmc-ibm-12.smt
index 583be85f9..583be85f9 100644
--- a/test/regress/bmc-ibm-12.smt
+++ b/test/regress/regress2/bmc-ibm-12.smt
diff --git a/test/regress/bmc-ibm-13.smt b/test/regress/regress2/bmc-ibm-13.smt
index bfe2bbbbc..bfe2bbbbc 100644
--- a/test/regress/bmc-ibm-13.smt
+++ b/test/regress/regress2/bmc-ibm-13.smt
diff --git a/test/regress/bmc-ibm-2.smt b/test/regress/regress2/bmc-ibm-2.smt
index 5f90bc620..5f90bc620 100644
--- a/test/regress/bmc-ibm-2.smt
+++ b/test/regress/regress2/bmc-ibm-2.smt
diff --git a/test/regress/bmc-ibm-3.smt b/test/regress/regress2/bmc-ibm-3.smt
index 8718a90d5..8718a90d5 100644
--- a/test/regress/bmc-ibm-3.smt
+++ b/test/regress/regress2/bmc-ibm-3.smt
diff --git a/test/regress/bmc-ibm-4.smt b/test/regress/regress2/bmc-ibm-4.smt
index 32c02308b..32c02308b 100644
--- a/test/regress/bmc-ibm-4.smt
+++ b/test/regress/regress2/bmc-ibm-4.smt
diff --git a/test/regress/bmc-ibm-5.smt b/test/regress/regress2/bmc-ibm-5.smt
index ba9020762..ba9020762 100644
--- a/test/regress/bmc-ibm-5.smt
+++ b/test/regress/regress2/bmc-ibm-5.smt
diff --git a/test/regress/bmc-ibm-6.smt b/test/regress/regress2/bmc-ibm-6.smt
index f0b583af8..f0b583af8 100644
--- a/test/regress/bmc-ibm-6.smt
+++ b/test/regress/regress2/bmc-ibm-6.smt
diff --git a/test/regress/bmc-ibm-7.smt b/test/regress/regress2/bmc-ibm-7.smt
index 3e8fd9321..3e8fd9321 100644
--- a/test/regress/bmc-ibm-7.smt
+++ b/test/regress/regress2/bmc-ibm-7.smt
diff --git a/test/regress/friedman_n6_i4.smt b/test/regress/regress2/friedman_n6_i4.smt
index 113877982..113877982 100644
--- a/test/regress/friedman_n6_i4.smt
+++ b/test/regress/regress2/friedman_n6_i4.smt
diff --git a/test/regress/hole9.cvc b/test/regress/regress2/hole9.cvc
index e6a0d420b..e6a0d420b 100644
--- a/test/regress/hole9.cvc
+++ b/test/regress/regress2/hole9.cvc
diff --git a/test/regress/qwh.35.405.shuffled-as.sat03-1651.smt b/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt
index 7c09b58aa..7c09b58aa 100644
--- a/test/regress/qwh.35.405.shuffled-as.sat03-1651.smt
+++ b/test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt
diff --git a/test/regress/C880mul.miter.shuffled-as.sat03-348.smt b/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt
index 0cce52b17..0cce52b17 100644
--- a/test/regress/C880mul.miter.shuffled-as.sat03-348.smt
+++ b/test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt
diff --git a/test/regress/comb2.shuffled-as.sat03-420.smt b/test/regress/regress3/comb2.shuffled-as.sat03-420.smt
index 19d6e6e24..19d6e6e24 100644
--- a/test/regress/comb2.shuffled-as.sat03-420.smt
+++ b/test/regress/regress3/comb2.shuffled-as.sat03-420.smt
diff --git a/test/regress/hole10.cvc b/test/regress/regress3/hole10.cvc
index 22adeda67..22adeda67 100644
--- a/test/regress/hole10.cvc
+++ b/test/regress/regress3/hole10.cvc
diff --git a/test/regress/instance_1151.smt b/test/regress/regress3/instance_1151.smt
index 0d5bd0beb..0d5bd0beb 100644
--- a/test/regress/instance_1151.smt
+++ b/test/regress/regress3/instance_1151.smt