summaryrefslogtreecommitdiff
path: root/test/regress/regress1/test12.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/test12.cvc')
-rw-r--r--test/regress/regress1/test12.cvc178
1 files changed, 0 insertions, 178 deletions
diff --git a/test/regress/regress1/test12.cvc b/test/regress/regress1/test12.cvc
deleted file mode 100644
index 39ced0428..000000000
--- a/test/regress/regress1/test12.cvc
+++ /dev/null
@@ -1,178 +0,0 @@
-% COMMAND-LINE: --incremental
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: not_entailed
-% EXPECT: entailed
-% EXPECT: entailed
-% EXPECT: entailed
-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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback