diff options
-rw-r--r-- | test/regress/logops.cvc | 14 | ||||
-rw-r--r-- | test/regress/regress0/boolean.cvc (renamed from test/regress/boolean.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/bug1.cvc (renamed from test/regress/bug1.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/hole6.cvc (renamed from test/regress/hole6.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/logops.cvc | 14 | ||||
-rw-r--r-- | test/regress/regress0/queries0.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/simple-uf.smt (renamed from test/regress/simple-uf.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress0/simple.cvc (renamed from test/regress/simple.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/simple.smt (renamed from test/regress/simple.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress0/simple2.smt (renamed from test/regress/simple2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress0/smallcnf.cvc | 9 | ||||
-rw-r--r-- | test/regress/regress0/test11.cvc (renamed from test/regress/test11.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/test12.cvc (renamed from test/regress/test12.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/test9.cvc (renamed from test/regress/test9.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/uf20-03.cvc (renamed from test/regress/uf20-03.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress0/wiki.cvc (renamed from test/regress/wiki.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress1/friedman_n4_i5.smt (renamed from test/regress/friedman_n4_i5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress1/hole7.cvc (renamed from test/regress/hole7.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress1/hole8.cvc (renamed from test/regress/hole8.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress1/instance_1444.smt (renamed from test/regress/instance_1444.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-galileo-8.smt (renamed from test/regress/bmc-galileo-8.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-galileo-9.smt (renamed from test/regress/bmc-galileo-9.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-1.smt (renamed from test/regress/bmc-ibm-1.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-10.smt (renamed from test/regress/bmc-ibm-10.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-11.smt (renamed from test/regress/bmc-ibm-11.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-12.smt (renamed from test/regress/bmc-ibm-12.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-13.smt (renamed from test/regress/bmc-ibm-13.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-2.smt (renamed from test/regress/bmc-ibm-2.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-3.smt (renamed from test/regress/bmc-ibm-3.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-4.smt (renamed from test/regress/bmc-ibm-4.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-5.smt (renamed from test/regress/bmc-ibm-5.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-6.smt (renamed from test/regress/bmc-ibm-6.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/bmc-ibm-7.smt (renamed from test/regress/bmc-ibm-7.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/friedman_n6_i4.smt (renamed from test/regress/friedman_n6_i4.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress2/hole9.cvc (renamed from test/regress/hole9.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress2/qwh.35.405.shuffled-as.sat03-1651.smt (renamed from test/regress/qwh.35.405.shuffled-as.sat03-1651.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/C880mul.miter.shuffled-as.sat03-348.smt (renamed from test/regress/C880mul.miter.shuffled-as.sat03-348.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/comb2.shuffled-as.sat03-420.smt (renamed from test/regress/comb2.shuffled-as.sat03-420.smt) | 0 | ||||
-rw-r--r-- | test/regress/regress3/hole10.cvc (renamed from test/regress/hole10.cvc) | 0 | ||||
-rw-r--r-- | test/regress/regress3/instance_1151.smt (renamed from test/regress/instance_1151.smt) | 0 |
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 |