summaryrefslogtreecommitdiff
path: root/test/regress/regress0/unconstrained
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/unconstrained')
-rw-r--r--test/regress/regress0/unconstrained/Makefile.am4
-rw-r--r--test/regress/regress0/unconstrained/mult1.smt28
2 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index a262499b8..4136566a0 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -71,7 +71,9 @@ TESTS = \
lt.smt2 \
uf1.smt2 \
uf2.smt2 \
- xor.smt2
+ xor.smt2
+
+# mult1.smt2
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/unconstrained/mult1.smt2 b/test/regress/regress0/unconstrained/mult1.smt2
new file mode 100644
index 000000000..fdad322af
--- /dev/null
+++ b/test/regress/regress0/unconstrained/mult1.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+
+(declare-fun x3 () Int)
+(assert (<= (* 1 x3) 0))
+
+(check-sat)
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback