summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress')
-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