summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-10-02 05:52:51 +0000
committerTim King <taking@cs.nyu.edu>2010-10-02 05:52:51 +0000
commit37c20e30239e8ce86e9fc7106afcf5a7b896e7c3 (patch)
treeee78b955ccfe0240d878945e7eb2baaeb5a9ed6b /test/regress/regress0/arith
parent02c2038dca9ce3e09cac66ed3bd6f8e2832ff74b (diff)
branches/arith-indexed-variables merged into the main trunk.
Diffstat (limited to 'test/regress/regress0/arith')
-rw-r--r--test/regress/regress0/arith/Makefile.am3
-rw-r--r--test/regress/regress0/arith/leq.01.smt6
2 files changed, 8 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 18ca5fe86..f38413d95 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -6,7 +6,8 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
TESTS = \
arith.01.cvc \
arith.02.cvc \
- arith.03.cvc
+ arith.03.cvc \
+ leq.01.smt
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/arith/leq.01.smt b/test/regress/regress0/arith/leq.01.smt
new file mode 100644
index 000000000..8cb08848b
--- /dev/null
+++ b/test/regress/regress0/arith/leq.01.smt
@@ -0,0 +1,6 @@
+(benchmark fuzzsmt
+:logic QF_LRA
+:status unsat
+:formula
+(<= 3 (~ 3))
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback