1 files changed, 151 insertions, 0 deletions
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;