summaryrefslogtreecommitdiff
path: root/test/regress/regress0
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-02-04 21:01:04 +0000
committerTim King <taking@cs.nyu.edu>2010-02-04 21:01:04 +0000
commitc6f86de8077f667ab2b2e9aac53d60d93ea2da93 (patch)
tree028e32de75592993169290f4cdf0cd27a447d89c /test/regress/regress0
parent3203c9bf8ec818b287c8b4030bb4b71d48ede9f1 (diff)
Moved regressions into various levels based on running time.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r--test/regress/regress0/boolean.cvc809
-rw-r--r--test/regress/regress0/bug1.cvc11
-rw-r--r--test/regress/regress0/hole6.cvc182
-rw-r--r--test/regress/regress0/logops.cvc14
-rw-r--r--test/regress/regress0/queries0.cvc11
-rw-r--r--test/regress/regress0/simple-uf.smt7
-rw-r--r--test/regress/regress0/simple.cvc6
-rw-r--r--test/regress/regress0/simple.smt15
-rw-r--r--test/regress/regress0/simple2.smt13
-rw-r--r--test/regress/regress0/smallcnf.cvc9
-rw-r--r--test/regress/regress0/test11.cvc11
-rw-r--r--test/regress/regress0/test12.cvc151
-rw-r--r--test/regress/regress0/test9.cvc7
-rw-r--r--test/regress/regress0/uf20-03.cvc118
-rw-r--r--test/regress/regress0/wiki.cvc38
15 files changed, 1402 insertions, 0 deletions
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
new file mode 100644
index 000000000..ac9885703
--- /dev/null
+++ b/test/regress/regress0/boolean.cvc
@@ -0,0 +1,809 @@
+%% Regression level = 1
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+p : BOOLEAN;
+q : BOOLEAN;
+r : BOOLEAN;
+s : BOOLEAN;
+t : BOOLEAN;
+u : BOOLEAN;
+v : BOOLEAN;
+P1 : BOOLEAN;
+P2 : BOOLEAN;
+P3 : BOOLEAN;
+P4 : BOOLEAN;
+P6 : BOOLEAN;
+P5 : BOOLEAN;
+a41 : BOOLEAN =
+ IF p THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a42 : BOOLEAN =
+ IF a41 THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a45 : BOOLEAN =
+ IF p THEN p
+ ELSE a41
+ ENDIF;
+a46 : BOOLEAN =
+ IF q THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a49 : BOOLEAN =
+ IF s THEN t
+ ELSE FALSE
+ ENDIF;
+a58 : BOOLEAN =
+ IF q THEN q
+ ELSE a46
+ ENDIF;
+a59 : BOOLEAN =
+ IF r THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a61 : BOOLEAN =
+ IF s THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a62 : BOOLEAN =
+ IF s THEN s
+ ELSE a61
+ ENDIF;
+a65 : BOOLEAN =
+ IF t THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a67 : BOOLEAN =
+ IF u THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a73 : BOOLEAN =
+ IF p THEN q
+ ELSE FALSE
+ ENDIF;
+a74 : BOOLEAN =
+ IF q THEN p
+ ELSE FALSE
+ ENDIF;
+a77 : BOOLEAN =
+ IF r THEN TRUE
+ ELSE s
+ ENDIF;
+a78 : BOOLEAN =
+ IF s THEN TRUE
+ ELSE r
+ ENDIF;
+a81 : BOOLEAN =
+ IF t THEN u
+ ELSE a67
+ ENDIF;
+a82 : BOOLEAN =
+ IF u THEN t
+ ELSE a65
+ ENDIF;
+a88 : BOOLEAN =
+ IF q THEN r
+ ELSE FALSE
+ ENDIF;
+a89 : BOOLEAN =
+ IF p THEN a88
+ ELSE FALSE
+ ENDIF;
+a92 : BOOLEAN =
+ IF s THEN TRUE
+ ELSE t
+ ENDIF;
+a94 : BOOLEAN =
+ IF t THEN TRUE
+ ELSE u
+ ENDIF;
+a95 : BOOLEAN =
+ IF s THEN TRUE
+ ELSE a94
+ ENDIF;
+a105 : BOOLEAN =
+ IF t THEN u
+ ELSE FALSE
+ ENDIF;
+a111 : BOOLEAN =
+ IF p THEN q
+ ELSE TRUE
+ ENDIF;
+a112 : BOOLEAN =
+ IF q THEN r
+ ELSE TRUE
+ ENDIF;
+a114 : BOOLEAN =
+ IF p THEN r
+ ELSE TRUE
+ ENDIF;
+a116 : BOOLEAN =
+ IF s THEN t
+ ELSE a65
+ ENDIF;
+a121 : BOOLEAN =
+ IF a46 THEN a41
+ ELSE TRUE
+ ENDIF;
+a126 : BOOLEAN =
+ IF a59 THEN a61
+ ELSE
+ IF a61 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF;
+a130 : BOOLEAN =
+ IF q THEN TRUE
+ ELSE r
+ ENDIF;
+a132 : BOOLEAN =
+ IF p THEN r
+ ELSE FALSE
+ ENDIF;
+a133 : BOOLEAN =
+ IF a73 THEN TRUE
+ ELSE a132
+ ENDIF;
+a138 : BOOLEAN =
+ IF a92 THEN
+ IF s THEN TRUE
+ ELSE u
+ ENDIF
+ ELSE FALSE
+ ENDIF;
+a143 : BOOLEAN =
+ IF a114 THEN a112
+ ELSE FALSE
+ ENDIF;
+a145 : BOOLEAN =
+ IF
+ IF
+ IF p THEN TRUE
+ ELSE q
+ ENDIF THEN r
+ ELSE TRUE
+ ENDIF THEN a143
+ ELSE
+ IF a143 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF;
+a147 : BOOLEAN =
+ IF s THEN t
+ ELSE TRUE
+ ENDIF;
+a148 : BOOLEAN =
+ IF s THEN u
+ ELSE TRUE
+ ENDIF;
+a149 : BOOLEAN =
+ IF a147 THEN TRUE
+ ELSE a148
+ ENDIF;
+a153 : BOOLEAN =
+ IF a73 THEN r
+ ELSE TRUE
+ ENDIF;
+a154 : BOOLEAN =
+ IF a114 THEN TRUE
+ ELSE a112
+ ENDIF;
+a158 : BOOLEAN =
+ IF a147 THEN a148
+ ELSE FALSE
+ ENDIF;
+a162 : BOOLEAN =
+ IF p THEN a112
+ ELSE TRUE
+ ENDIF;
+a167 : BOOLEAN =
+ IF a46 THEN TRUE
+ ELSE a59
+ ENDIF;
+a171 : BOOLEAN =
+ IF a61 THEN a65
+ ELSE FALSE
+ ENDIF;
+a176 : BOOLEAN =
+ IF p THEN q
+ ELSE r
+ ENDIF;
+a178 : BOOLEAN =
+ IF p THEN a46
+ ELSE a59
+ ENDIF;
+a183 : BOOLEAN =
+ IF s THEN a65
+ ELSE
+ IF a65 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF;
+a187 : BOOLEAN =
+ IF a41 THEN TRUE
+ ELSE q
+ ENDIF;
+a192 : BOOLEAN =
+ IF
+ IF r THEN s
+ ELSE FALSE
+ ENDIF THEN TRUE
+ ELSE
+ IF a59 THEN t
+ ELSE FALSE
+ ENDIF
+ ENDIF;
+a197 : BOOLEAN =
+ IF a111 THEN
+ IF a41 THEN r
+ ELSE TRUE
+ ENDIF
+ ELSE FALSE
+ ENDIF;
+a200 : BOOLEAN =
+ IF a49 THEN TRUE
+ ELSE a171
+ ENDIF;
+a204 : BOOLEAN =
+ IF p THEN q
+ ELSE a46
+ ENDIF;
+a205 : BOOLEAN =
+ IF q THEN p
+ ELSE TRUE
+ ENDIF;
+a206 : BOOLEAN =
+ IF a111 THEN a205
+ ELSE FALSE
+ ENDIF;
+a210 : BOOLEAN =
+ IF p THEN a46
+ ELSE TRUE
+ ENDIF;
+a214 : BOOLEAN =
+ IF a73 THEN FALSE
+ ELSE TRUE
+ ENDIF;
+a221 : BOOLEAN =
+ IF
+ IF p THEN a46
+ ELSE FALSE
+ ENDIF THEN r
+ ELSE TRUE
+ ENDIF;
+a225 : BOOLEAN =
+ IF a187 THEN a132
+ ELSE TRUE
+ ENDIF;
+a228 : BOOLEAN =
+ IF q THEN r
+ ELSE a59
+ ENDIF;
+a231 : BOOLEAN =
+ IF a204 THEN r
+ ELSE a59
+ ENDIF;
+a237 : BOOLEAN =
+ IF q THEN a132
+ ELSE
+ IF a41 THEN s
+ ELSE FALSE
+ ENDIF
+ ENDIF;
+a288 : BOOLEAN =
+ IF
+ IF
+ IF p THEN a41
+ ELSE a42
+ ENDIF THEN FALSE
+ ELSE TRUE
+ ENDIF THEN
+ IF
+ IF a45 THEN
+ IF
+ IF q THEN TRUE
+ ELSE a46
+ ENDIF THEN
+ IF
+ IF r THEN r
+ ELSE TRUE
+ ENDIF THEN
+ IF
+ IF a49 THEN s
+ ELSE TRUE
+ ENDIF THEN
+ IF u THEN
+ IF u THEN TRUE
+ ELSE v
+ ENDIF
+ ELSE TRUE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF a58 THEN
+ IF
+ IF r THEN r
+ ELSE a59
+ ENDIF THEN a62
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF a45 THEN
+ IF a62 THEN
+ IF
+ IF t THEN t
+ ELSE a65
+ ENDIF THEN
+ IF a67 THEN a67
+ ELSE
+ IF a67 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF a73 THEN a74
+ ELSE
+ IF a74 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a77 THEN a78
+ ELSE
+ IF a78 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF a81 THEN a82
+ ELSE
+ IF a82 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF
+ IF a73 THEN r
+ ELSE FALSE
+ ENDIF THEN a89
+ ELSE
+ IF a89 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a92 THEN TRUE
+ ELSE u
+ ENDIF THEN a95
+ ELSE
+ IF a95 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF
+ IF p THEN p
+ ELSE FALSE
+ ENDIF THEN p
+ ELSE a41
+ ENDIF THEN
+ IF
+ IF
+ IF q THEN TRUE
+ ELSE q
+ ENDIF THEN q
+ ELSE a46
+ ENDIF THEN
+ IF
+ IF
+ IF r THEN a77
+ ELSE FALSE
+ ENDIF THEN r
+ ELSE a59
+ ENDIF THEN
+ IF
+ IF t THEN TRUE
+ ELSE a105
+ ENDIF THEN t
+ ELSE a65
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF a58 THEN
+ IF
+ IF
+ IF
+ IF a111 THEN a112
+ ELSE FALSE
+ ENDIF THEN a114
+ ELSE TRUE
+ ENDIF THEN
+ IF
+ IF a116 THEN a81
+ ELSE FALSE
+ ENDIF THEN
+ IF s THEN u
+ ELSE a67
+ ENDIF
+ ELSE TRUE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF a111 THEN a121
+ ELSE
+ IF a121 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF r THEN s
+ ELSE a61
+ ENDIF THEN a126
+ ELSE
+ IF a126 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF
+ IF p THEN a130
+ ELSE FALSE
+ ENDIF THEN a133
+ ELSE
+ IF a133 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF s THEN TRUE
+ ELSE a105
+ ENDIF THEN a138
+ ELSE
+ IF a138 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF a145 THEN
+ IF
+ IF s THEN a94
+ ELSE TRUE
+ ENDIF THEN a149
+ ELSE
+ IF a149 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF a153 THEN a154
+ ELSE
+ IF a154 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF s THEN a105
+ ELSE TRUE
+ ENDIF THEN a158
+ ELSE
+ IF a158 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF a153 THEN a162
+ ELSE
+ IF a162 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF a42 THEN p
+ ELSE a41
+ ENDIF THEN
+ IF
+ IF
+ IF a88 THEN FALSE
+ ELSE TRUE
+ ENDIF THEN a167
+ ELSE
+ IF a167 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a92 THEN FALSE
+ ELSE TRUE
+ ENDIF THEN a171
+ ELSE
+ IF a171 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF
+ IF a176 THEN FALSE
+ ELSE TRUE
+ ENDIF THEN a178
+ ELSE
+ IF a178 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a116 THEN FALSE
+ ELSE TRUE
+ ENDIF THEN a183
+ ELSE
+ IF a183 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF a111 THEN a187
+ ELSE
+ IF a187 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF r THEN s
+ ELSE t
+ ENDIF THEN a192
+ ELSE
+ IF a192 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF
+ IF a176 THEN a197
+ ELSE
+ IF a197 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF a116 THEN a200
+ ELSE
+ IF a200 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF a204 THEN a206
+ ELSE
+ IF a206 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a111 THEN TRUE
+ ELSE a205
+ ENDIF THEN
+ IF
+ IF a46 THEN TRUE
+ ELSE
+ IF
+ IF a210 THEN p
+ ELSE FALSE
+ ENDIF THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF a210 THEN a214
+ ELSE
+ IF a214 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF a145 THEN
+ IF
+ IF a162 THEN a153
+ ELSE
+ IF a153 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF p THEN a130
+ ELSE TRUE
+ ENDIF THEN a221
+ ELSE
+ IF a221 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF p THEN a112
+ ELSE FALSE
+ ENDIF THEN a225
+ ELSE
+ IF a225 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF p THEN a228
+ ELSE
+ IF a228 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN a231
+ ELSE
+ IF a231 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF p THEN a88
+ ELSE
+ IF a46 THEN s
+ ELSE FALSE
+ ENDIF
+ ENDIF THEN a237
+ ELSE
+ IF a237 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF P1 THEN
+ IF P2 THEN TRUE
+ ELSE P3
+ ENDIF
+ ELSE
+ IF P3 THEN TRUE
+ ELSE P4
+ ENDIF
+ ENDIF THEN
+ IF
+ IF P3 THEN
+ IF P6 THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ELSE
+ IF P4 THEN P1
+ ELSE TRUE
+ ENDIF
+ ENDIF THEN
+ IF
+ IF
+ IF P2 THEN P5
+ ELSE FALSE
+ ENDIF THEN FALSE
+ ELSE TRUE
+ ENDIF THEN
+ IF P2 THEN P5
+ ELSE TRUE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF THEN
+ IF
+ IF P3 THEN P6
+ ELSE TRUE
+ ENDIF THEN FALSE
+ ELSE TRUE
+ ENDIF
+ ELSE TRUE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF
+ ELSE FALSE
+ ENDIF;
+QUERY a288;
diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc
new file mode 100644
index 000000000..d2c24a438
--- /dev/null
+++ b/test/regress/regress0/bug1.cvc
@@ -0,0 +1,11 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+x : REAL;
+y : REAL;
+f : REAL -> REAL;
+ASSERT ((x > y) => f(x) > f (y));
+ASSERT (x = 3);
+ASSERT (y = 2);
+QUERY(f(x) > f (y));
diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
new file mode 100644
index 000000000..28738fc24
--- /dev/null
+++ b/test/regress/regress0/hole6.cvc
@@ -0,0 +1,182 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+x_1 : BOOLEAN;
+x_2 : BOOLEAN;
+x_3 : BOOLEAN;
+x_4 : BOOLEAN;
+x_5 : BOOLEAN;
+x_6 : BOOLEAN;
+x_7 : BOOLEAN;
+x_8 : BOOLEAN;
+x_9 : BOOLEAN;
+x_10 : BOOLEAN;
+x_11 : BOOLEAN;
+x_12 : BOOLEAN;
+x_13 : BOOLEAN;
+x_14 : BOOLEAN;
+x_15 : BOOLEAN;
+x_16 : BOOLEAN;
+x_17 : BOOLEAN;
+x_18 : BOOLEAN;
+x_19 : BOOLEAN;
+x_20 : BOOLEAN;
+x_21 : BOOLEAN;
+x_22 : BOOLEAN;
+x_23 : BOOLEAN;
+x_24 : BOOLEAN;
+x_25 : BOOLEAN;
+x_26 : BOOLEAN;
+x_27 : BOOLEAN;
+x_28 : BOOLEAN;
+x_29 : BOOLEAN;
+x_30 : BOOLEAN;
+x_31 : BOOLEAN;
+x_32 : BOOLEAN;
+x_33 : BOOLEAN;
+x_34 : BOOLEAN;
+x_35 : BOOLEAN;
+x_36 : BOOLEAN;
+x_37 : BOOLEAN;
+x_38 : BOOLEAN;
+x_39 : BOOLEAN;
+x_40 : BOOLEAN;
+x_41 : BOOLEAN;
+x_42 : BOOLEAN;
+ASSERT NOT x_1 OR NOT x_7;
+ASSERT NOT x_1 OR NOT x_13;
+ASSERT NOT x_1 OR NOT x_19;
+ASSERT NOT x_1 OR NOT x_25;
+ASSERT NOT x_1 OR NOT x_31;
+ASSERT NOT x_1 OR NOT x_37;
+ASSERT NOT x_7 OR NOT x_13;
+ASSERT NOT x_7 OR NOT x_19;
+ASSERT NOT x_7 OR NOT x_25;
+ASSERT NOT x_7 OR NOT x_31;
+ASSERT NOT x_7 OR NOT x_37;
+ASSERT NOT x_13 OR NOT x_19;
+ASSERT NOT x_13 OR NOT x_25;
+ASSERT NOT x_13 OR NOT x_31;
+ASSERT NOT x_13 OR NOT x_37;
+ASSERT NOT x_19 OR NOT x_25;
+ASSERT NOT x_19 OR NOT x_31;
+ASSERT NOT x_19 OR NOT x_37;
+ASSERT NOT x_25 OR NOT x_31;
+ASSERT NOT x_25 OR NOT x_37;
+ASSERT NOT x_31 OR NOT x_37;
+ASSERT NOT x_2 OR NOT x_8;
+ASSERT NOT x_2 OR NOT x_14;
+ASSERT NOT x_2 OR NOT x_20;
+ASSERT NOT x_2 OR NOT x_26;
+ASSERT NOT x_2 OR NOT x_32;
+ASSERT NOT x_2 OR NOT x_38;
+ASSERT NOT x_8 OR NOT x_14;
+ASSERT NOT x_8 OR NOT x_20;
+ASSERT NOT x_8 OR NOT x_26;
+ASSERT NOT x_8 OR NOT x_32;
+ASSERT NOT x_8 OR NOT x_38;
+ASSERT NOT x_14 OR NOT x_20;
+ASSERT NOT x_14 OR NOT x_26;
+ASSERT NOT x_14 OR NOT x_32;
+ASSERT NOT x_14 OR NOT x_38;
+ASSERT NOT x_20 OR NOT x_26;
+ASSERT NOT x_20 OR NOT x_32;
+ASSERT NOT x_20 OR NOT x_38;
+ASSERT NOT x_26 OR NOT x_32;
+ASSERT NOT x_26 OR NOT x_38;
+ASSERT NOT x_32 OR NOT x_38;
+ASSERT NOT x_3 OR NOT x_9;
+ASSERT NOT x_3 OR NOT x_15;
+ASSERT NOT x_3 OR NOT x_21;
+ASSERT NOT x_3 OR NOT x_27;
+ASSERT NOT x_3 OR NOT x_33;
+ASSERT NOT x_3 OR NOT x_39;
+ASSERT NOT x_9 OR NOT x_15;
+ASSERT NOT x_9 OR NOT x_21;
+ASSERT NOT x_9 OR NOT x_27;
+ASSERT NOT x_9 OR NOT x_33;
+ASSERT NOT x_9 OR NOT x_39;
+ASSERT NOT x_15 OR NOT x_21;
+ASSERT NOT x_15 OR NOT x_27;
+ASSERT NOT x_15 OR NOT x_33;
+ASSERT NOT x_15 OR NOT x_39;
+ASSERT NOT x_21 OR NOT x_27;
+ASSERT NOT x_21 OR NOT x_33;
+ASSERT NOT x_21 OR NOT x_39;
+ASSERT NOT x_27 OR NOT x_33;
+ASSERT NOT x_27 OR NOT x_39;
+ASSERT NOT x_33 OR NOT x_39;
+ASSERT NOT x_4 OR NOT x_10;
+ASSERT NOT x_4 OR NOT x_16;
+ASSERT NOT x_4 OR NOT x_22;
+ASSERT NOT x_4 OR NOT x_28;
+ASSERT NOT x_4 OR NOT x_34;
+ASSERT NOT x_4 OR NOT x_40;
+ASSERT NOT x_10 OR NOT x_16;
+ASSERT NOT x_10 OR NOT x_22;
+ASSERT NOT x_10 OR NOT x_28;
+ASSERT NOT x_10 OR NOT x_34;
+ASSERT NOT x_10 OR NOT x_40;
+ASSERT NOT x_16 OR NOT x_22;
+ASSERT NOT x_16 OR NOT x_28;
+ASSERT NOT x_16 OR NOT x_34;
+ASSERT NOT x_16 OR NOT x_40;
+ASSERT NOT x_22 OR NOT x_28;
+ASSERT NOT x_22 OR NOT x_34;
+ASSERT NOT x_22 OR NOT x_40;
+ASSERT NOT x_28 OR NOT x_34;
+ASSERT NOT x_28 OR NOT x_40;
+ASSERT NOT x_34 OR NOT x_40;
+ASSERT NOT x_5 OR NOT x_11;
+ASSERT NOT x_5 OR NOT x_17;
+ASSERT NOT x_5 OR NOT x_23;
+ASSERT NOT x_5 OR NOT x_29;
+ASSERT NOT x_5 OR NOT x_35;
+ASSERT NOT x_5 OR NOT x_41;
+ASSERT NOT x_11 OR NOT x_17;
+ASSERT NOT x_11 OR NOT x_23;
+ASSERT NOT x_11 OR NOT x_29;
+ASSERT NOT x_11 OR NOT x_35;
+ASSERT NOT x_11 OR NOT x_41;
+ASSERT NOT x_17 OR NOT x_23;
+ASSERT NOT x_17 OR NOT x_29;
+ASSERT NOT x_17 OR NOT x_35;
+ASSERT NOT x_17 OR NOT x_41;
+ASSERT NOT x_23 OR NOT x_29;
+ASSERT NOT x_23 OR NOT x_35;
+ASSERT NOT x_23 OR NOT x_41;
+ASSERT NOT x_29 OR NOT x_35;
+ASSERT NOT x_29 OR NOT x_41;
+ASSERT NOT x_35 OR NOT x_41;
+ASSERT NOT x_6 OR NOT x_12;
+ASSERT NOT x_6 OR NOT x_18;
+ASSERT NOT x_6 OR NOT x_24;
+ASSERT NOT x_6 OR NOT x_30;
+ASSERT NOT x_6 OR NOT x_36;
+ASSERT NOT x_6 OR NOT x_42;
+ASSERT NOT x_12 OR NOT x_18;
+ASSERT NOT x_12 OR NOT x_24;
+ASSERT NOT x_12 OR NOT x_30;
+ASSERT NOT x_12 OR NOT x_36;
+ASSERT NOT x_12 OR NOT x_42;
+ASSERT NOT x_18 OR NOT x_24;
+ASSERT NOT x_18 OR NOT x_30;
+ASSERT NOT x_18 OR NOT x_36;
+ASSERT NOT x_18 OR NOT x_42;
+ASSERT NOT x_24 OR NOT x_30;
+ASSERT NOT x_24 OR NOT x_36;
+ASSERT NOT x_24 OR NOT x_42;
+ASSERT NOT x_30 OR NOT x_36;
+ASSERT NOT x_30 OR NOT x_42;
+ASSERT NOT x_36 OR NOT x_42;
+ASSERT x_6 OR x_5 OR x_4 OR x_3 OR x_2 OR x_1;
+ASSERT x_12 OR x_11 OR x_10 OR x_9 OR x_8 OR x_7;
+ASSERT x_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13;
+ASSERT x_24 OR x_23 OR x_22 OR x_21 OR x_20 OR x_19;
+ASSERT x_30 OR x_29 OR x_28 OR x_27 OR x_26 OR x_25;
+ASSERT x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31;
+ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
+
+
+QUERY FALSE;
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/regress0/simple-uf.smt b/test/regress/regress0/simple-uf.smt
new file mode 100644
index 000000000..3aaba2ab0
--- /dev/null
+++ b/test/regress/regress0/simple-uf.smt
@@ -0,0 +1,7 @@
+(benchmark simple_uf
+ :logic QF_UF
+ :extrasorts (A B)
+ :extrafuns ((f A B) (x A) (y A))
+ :formula (not (implies (= x y) (= (f x) (f y))))
+ :status unsat
+)
diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc
new file mode 100644
index 000000000..3566053d9
--- /dev/null
+++ b/test/regress/regress0/simple.cvc
@@ -0,0 +1,6 @@
+x0, x1, x2, x3 : BOOLEAN;
+ASSERT x1 OR NOT x0;
+ASSERT x0 OR NOT x3;
+ASSERT x3 OR x2;
+ASSERT x1 AND NOT x1;
+QUERY x2;
diff --git a/test/regress/regress0/simple.smt b/test/regress/regress0/simple.smt
new file mode 100644
index 000000000..56aa82d72
--- /dev/null
+++ b/test/regress/regress0/simple.smt
@@ -0,0 +1,15 @@
+(benchmark b
+:status unknown
+:logic QF_UF
+:extrapreds ((x0))
+:extrapreds ((x1))
+:extrapreds ((x2))
+:extrapreds ((x3))
+:formula
+(and (or x1 (not x0))
+ (or x0 (not x3))
+ (or x3 x2)
+ (not x1)
+ x2
+ x3)
+)
diff --git a/test/regress/regress0/simple2.smt b/test/regress/regress0/simple2.smt
new file mode 100644
index 000000000..e917d1b64
--- /dev/null
+++ b/test/regress/regress0/simple2.smt
@@ -0,0 +1,13 @@
+(benchmark b
+:status unknown
+:logic QF_UF
+:extrapreds ((x0))
+:extrapreds ((x1))
+:extrapreds ((x2))
+:extrapreds ((x3))
+:formula
+(and (or x1 (not x0))
+ (or x0 (not x3))
+ (or x3 x2)
+ (not x1))
+)
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/regress0/test11.cvc b/test/regress/regress0/test11.cvc
new file mode 100644
index 000000000..ff0880b2a
--- /dev/null
+++ b/test/regress/regress0/test11.cvc
@@ -0,0 +1,11 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+
+x, y : BOOLEAN;
+
+ASSERT (x OR y);
+ASSERT NOT (x OR y);
+
+QUERY FALSE;
diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc
new file mode 100644
index 000000000..31ec0864e
--- /dev/null
+++ b/test/regress/regress0/test12.cvc
@@ -0,0 +1,151 @@
+%% Regression level = 1
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+A: TYPE;
+P_1: BOOLEAN;
+P_2: BOOLEAN;
+P_3: BOOLEAN;
+ASSERT (NOT P_1 OR P_2 OR P_2);
+ASSERT (NOT P_1 OR P_2 OR P_3);
+P_4: BOOLEAN;
+P_5: BOOLEAN;
+ASSERT (NOT P_1 OR NOT P_4 OR P_2);
+ASSERT (NOT P_1 OR NOT P_5 OR P_2);
+P_6: BOOLEAN;
+P_7: BOOLEAN;
+ASSERT (NOT P_2 OR P_6 OR P_1);
+ASSERT (NOT P_2 OR P_7 OR P_1);
+P_8: BOOLEAN;
+P_9: BOOLEAN;
+ASSERT (NOT P_2 OR NOT P_8 OR P_1);
+ASSERT (NOT P_2 OR NOT P_9 OR P_1);
+P_10: BOOLEAN;
+ASSERT (P_2 OR P_1 OR P_4);
+ASSERT (P_2 OR P_1 OR P_10);
+ASSERT (NOT P_2 OR NOT P_1 OR P_4);
+ASSERT (NOT P_2 OR NOT P_1 OR P_10);
+P_11: BOOLEAN;
+ASSERT (NOT P_6 OR P_2 OR P_1);
+ASSERT (NOT P_11 OR P_2 OR P_1);
+ASSERT (NOT P_6 OR NOT P_2 OR NOT P_1);
+ASSERT (NOT P_11 OR NOT P_2 OR NOT P_1);
+PUSH;
+QUERY (NOT P_2 OR NOT P_3);
+POP;
+PUSH;
+QUERY (P_1 OR NOT P_3);
+POP;
+PUSH;
+QUERY (NOT P_2 OR P_1);
+POP;
+PUSH;
+QUERY (P_5 OR NOT P_2);
+POP;
+PUSH;
+QUERY (P_1 OR NOT P_2);
+POP;
+PUSH;
+QUERY (P_5 OR P_1);
+POP;
+PUSH;
+QUERY (NOT P_7 OR NOT P_1);
+POP;
+PUSH;
+QUERY (P_2 OR NOT P_1);
+POP;
+PUSH;
+QUERY P_2;
+POP;
+PUSH;
+QUERY (P_9 OR NOT P_1);
+POP;
+PUSH;
+QUERY (P_2 OR NOT P_1);
+POP;
+PUSH;
+QUERY P_2;
+POP;
+PUSH;
+QUERY (NOT P_1 OR NOT P_10);
+POP;
+PUSH;
+QUERY (NOT P_2 OR NOT P_10);
+POP;
+PUSH;
+QUERY (NOT P_1 OR NOT P_2);
+POP;
+PUSH;
+QUERY (P_1 OR NOT P_10);
+POP;
+PUSH;
+QUERY (P_2 OR NOT P_10);
+POP;
+PUSH;
+QUERY (P_1 OR P_2);
+POP;
+PUSH;
+QUERY (NOT P_2 OR NOT P_1);
+POP;
+PUSH;
+QUERY (P_11 OR NOT P_1);
+POP;
+PUSH;
+QUERY (NOT P_2 OR P_11);
+POP;
+PUSH;
+QUERY (P_2 OR P_1);
+POP;
+PUSH;
+QUERY (P_11 OR P_1);
+POP;
+PUSH;
+QUERY (P_2 OR P_11);
+POP;
+P_12: BOOLEAN;
+ASSERT (NOT P_12 OR P_2);
+ASSERT (NOT P_12 OR P_3);
+ASSERT (P_12 OR NOT P_1 OR P_2);
+ASSERT (P_12 OR NOT P_1 OR P_2);
+P_13: BOOLEAN;
+ASSERT (NOT P_13 OR NOT P_4);
+ASSERT (NOT P_13 OR NOT P_5);
+ASSERT (P_13 OR NOT P_1 OR P_2);
+ASSERT (P_13 OR NOT P_1 OR P_2);
+ASSERT (NOT P_2 OR P_1);
+ASSERT (NOT P_2 OR P_1);
+ASSERT (NOT P_2 OR P_1);
+ASSERT (NOT P_2 OR P_1);
+P_14: BOOLEAN;
+ASSERT (P_14 OR P_2 OR P_1);
+ASSERT (P_14 OR P_2 OR P_1);
+ASSERT (NOT P_14 OR P_4);
+ASSERT (NOT P_14 OR P_10);
+ASSERT (P_14 OR NOT P_2 OR NOT P_1);
+ASSERT (P_14 OR NOT P_2 OR NOT P_1);
+P_15: BOOLEAN;
+ASSERT (P_15 OR P_2 OR P_1);
+ASSERT (P_15 OR P_2 OR P_1);
+ASSERT (NOT P_15 OR NOT P_6);
+ASSERT (NOT P_15 OR NOT P_11);
+ASSERT (P_15 OR NOT P_2 OR NOT P_1);
+ASSERT (P_15 OR NOT P_2 OR NOT P_1);
+PUSH;
+QUERY NOT P_3;
+POP;
+PUSH;
+QUERY P_12;
+POP;
+PUSH;
+QUERY P_11;
+POP;
+PUSH;
+QUERY P_15;
+POP;
+ASSERT NOT P_15;
+ASSERT NOT P_15;
+PUSH;
+QUERY NOT P_10;
+POP;
+PUSH;
+QUERY FALSE;
diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc
new file mode 100644
index 000000000..eabbc9774
--- /dev/null
+++ b/test/regress/regress0/test9.cvc
@@ -0,0 +1,7 @@
+%% Regression level = 0
+%% Result = Valid
+%% Runtime = 1
+%% Language = presentation
+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
new file mode 100644
index 000000000..5e7b22b64
--- /dev/null
+++ b/test/regress/regress0/uf20-03.cvc
@@ -0,0 +1,118 @@
+%% Regression level = 0
+%% Result = Invalid
+%% Runtime = 1
+%% Language = presentation
+x_1 : BOOLEAN;
+x_2 : BOOLEAN;
+x_3 : BOOLEAN;
+x_4 : BOOLEAN;
+x_5 : BOOLEAN;
+x_6 : BOOLEAN;
+x_7 : BOOLEAN;
+x_8 : BOOLEAN;
+x_9 : BOOLEAN;
+x_10 : BOOLEAN;
+x_11 : BOOLEAN;
+x_12 : BOOLEAN;
+x_13 : BOOLEAN;
+x_14 : BOOLEAN;
+x_15 : BOOLEAN;
+x_16 : BOOLEAN;
+x_17 : BOOLEAN;
+x_18 : BOOLEAN;
+x_19 : BOOLEAN;
+x_20 : BOOLEAN;
+ASSERT NOT x_9 OR x_3 OR NOT x_15;
+ASSERT NOT x_12 OR NOT x_4 OR NOT x_15;
+ASSERT x_6 OR x_14 OR NOT x_17;
+ASSERT x_10 OR x_16 OR x_11;
+ASSERT NOT x_15 OR x_20 OR NOT x_7;
+ASSERT NOT x_1 OR x_10 OR x_16;
+ASSERT x_13 OR x_17 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_14 OR NOT x_13;
+ASSERT x_13 OR NOT x_6 OR x_15;
+ASSERT NOT x_9 OR x_3 OR x_16;
+ASSERT NOT x_20 OR NOT x_13 OR x_4;
+ASSERT NOT x_7 OR x_15 OR NOT x_14;
+ASSERT NOT x_15 OR NOT x_16 OR x_6;
+ASSERT x_5 OR NOT x_18 OR x_20;
+ASSERT NOT x_16 OR NOT x_19 OR x_7;
+ASSERT x_20 OR NOT x_18 OR NOT x_2;
+ASSERT x_10 OR NOT x_19 OR NOT x_14;
+ASSERT x_16 OR NOT x_7 OR x_12;
+ASSERT x_6 OR NOT x_5 OR NOT x_1;
+ASSERT NOT x_9 OR x_11 OR x_15;
+ASSERT x_19 OR NOT x_6 OR x_7;
+ASSERT NOT x_11 OR x_17 OR NOT x_19;
+ASSERT x_9 OR NOT x_16 OR x_6;
+ASSERT x_15 OR NOT x_20 OR x_10;
+ASSERT x_9 OR NOT x_1 OR NOT x_11;
+ASSERT NOT x_8 OR NOT x_19 OR x_5;
+ASSERT NOT x_19 OR x_11 OR x_20;
+ASSERT NOT x_12 OR x_13 OR NOT x_3;
+ASSERT NOT x_7 OR NOT x_17 OR NOT x_19;
+ASSERT x_17 OR x_6 OR NOT x_11;
+ASSERT NOT x_7 OR NOT x_17 OR x_10;
+ASSERT NOT x_14 OR x_9 OR x_20;
+ASSERT x_1 OR NOT x_18 OR NOT x_16;
+ASSERT NOT x_2 OR NOT x_15 OR x_20;
+ASSERT x_14 OR x_18 OR NOT x_1;
+ASSERT NOT x_8 OR NOT x_4 OR x_1;
+ASSERT x_13 OR x_3 OR NOT x_9;
+ASSERT x_5 OR x_7 OR x_8;
+ASSERT x_9 OR x_4 OR NOT x_20;
+ASSERT NOT x_18 OR NOT x_15 OR NOT x_10;
+ASSERT x_10 OR x_3 OR NOT x_20;
+ASSERT x_20 OR NOT x_14 OR x_16;
+ASSERT x_20 OR NOT x_3 OR NOT x_11;
+ASSERT NOT x_12 OR x_19 OR NOT x_16;
+ASSERT NOT x_3 OR x_5 OR x_10;
+ASSERT x_8 OR x_13 OR NOT x_7;
+ASSERT NOT x_2 OR NOT x_15 OR x_10;
+ASSERT NOT x_3 OR x_9 OR x_16;
+ASSERT NOT x_12 OR NOT x_16 OR NOT x_18;
+ASSERT x_3 OR x_1 OR NOT x_12;
+ASSERT NOT x_18 OR x_13 OR x_5;
+ASSERT x_1 OR x_3 OR NOT x_19;
+ASSERT NOT x_19 OR NOT x_5 OR x_6;
+ASSERT NOT x_20 OR x_8 OR NOT x_2;
+ASSERT x_17 OR NOT x_8 OR NOT x_13;
+ASSERT x_7 OR NOT x_11 OR NOT x_12;
+ASSERT NOT x_10 OR NOT x_14 OR NOT x_20;
+ASSERT NOT x_1 OR x_16 OR NOT x_12;
+ASSERT x_5 OR NOT x_3 OR x_9;
+ASSERT NOT x_18 OR x_8 OR x_14;
+ASSERT x_1 OR x_16 OR x_12;
+ASSERT x_20 OR NOT x_1 OR NOT x_16;
+ASSERT x_5 OR x_10 OR NOT x_13;
+ASSERT x_9 OR NOT x_10 OR x_6;
+ASSERT NOT x_12 OR x_10 OR NOT x_14;
+ASSERT NOT x_13 OR x_1 OR x_4;
+ASSERT NOT x_20 OR NOT x_7 OR x_3;
+ASSERT x_12 OR x_1 OR NOT x_10;
+ASSERT NOT x_1 OR NOT x_16 OR x_7;
+ASSERT x_11 OR NOT x_6 OR NOT x_4;
+ASSERT x_1 OR x_16 OR NOT x_20;
+ASSERT x_9 OR x_7 OR x_15;
+ASSERT NOT x_6 OR x_17 OR x_10;
+ASSERT x_8 OR x_9 OR x_17;
+ASSERT x_18 OR x_11 OR x_10;
+ASSERT x_7 OR x_1 OR NOT x_8;
+ASSERT NOT x_5 OR NOT x_12 OR x_18;
+ASSERT NOT x_6 OR x_2 OR x_15;
+ASSERT x_2 OR x_18 OR x_1;
+ASSERT NOT x_7 OR NOT x_13 OR x_16;
+ASSERT x_18 OR x_19 OR x_9;
+ASSERT x_9 OR NOT x_14 OR x_18;
+ASSERT x_14 OR x_12 OR NOT x_5;
+ASSERT NOT x_13 OR NOT x_7 OR NOT x_14;
+ASSERT NOT x_1 OR x_8 OR NOT x_16;
+ASSERT NOT x_11 OR x_4 OR x_7;
+ASSERT NOT x_4 OR x_20 OR x_5;
+ASSERT NOT x_5 OR x_2 OR x_12;
+ASSERT NOT x_5 OR x_13 OR NOT x_18;
+ASSERT NOT x_18 OR x_9 OR x_1;
+ASSERT x_10 OR NOT x_11 OR x_16;
+
+
+QUERY FALSE;
diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc
new file mode 100644
index 000000000..ab888039e
--- /dev/null
+++ b/test/regress/regress0/wiki.cvc
@@ -0,0 +1,38 @@
+
+
+a, b, c : BOOLEAN;
+
+QUERY a OR (b OR c) <=> (a OR b) OR c;
+QUERY a AND (b AND c) <=> (a AND b) AND c;
+
+QUERY a OR b <=> b OR a;
+QUERY a AND b <=> b AND a;
+
+QUERY a OR (a AND b) <=> a;
+QUERY a AND (a OR b) <=> a;
+
+QUERY a OR (b AND c) <=> (a OR b) AND (a OR c);
+QUERY a AND (b OR c) <=> (a AND b) OR (a AND c);
+
+QUERY a OR NOT a;
+QUERY a AND NOT a <=> FALSE;
+
+QUERY a OR a <=> a;
+QUERY a AND a <=> a;
+
+
+QUERY a OR FALSE <=> a;
+QUERY a AND TRUE <=> a;
+
+QUERY a OR TRUE <=> TRUE;
+QUERY a AND FALSE <=> FALSE;
+
+QUERY NOT FALSE <=> TRUE;
+QUERY NOT TRUE <=> FALSE;
+
+QUERY NOT (a OR b) <=> NOT a AND NOT b;
+QUERY NOT (a AND b) <=> NOT a OR NOT b;
+
+QUERY NOT NOT a <=> a;
+
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback