summaryrefslogtreecommitdiff
path: root/test/regress/regress0/preprocess
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/preprocess')
-rw-r--r--test/regress/regress0/preprocess/Makefile.am3
-rw-r--r--test/regress/regress0/preprocess/preprocess_13.cvc10
2 files changed, 12 insertions, 1 deletions
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 96b5d2928..42f763f07 100644
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -37,7 +37,8 @@ CVC_TESTS = \
preprocess_09.cvc \
preprocess_10.cvc \
preprocess_11.cvc \
- preprocess_12.cvc
+ preprocess_12.cvc \
+ preprocess_13.cvc
# Regression tests derived from bug reports
BUG_TESTS =
diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc
new file mode 100644
index 000000000..7a2ed7dd8
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_13.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9))))))))));
+
+% EXIT: 20
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback