Adding an example that violates an assertion during unconstrained simplification.

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index a262499b866b6d07b0e7b9b732c4146d3e7ccc68..4136566a07860a1dd290e09947cc2cc7d720fcf7 100644 (file)
--- 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 (file)
index 0000000..fdad322
--- /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)