From be3732415376e78930a4b74145f0101324db4c15 Mon Sep 17 00:00:00 2001
From: Tim King <tim.king@imag.fr>
Date: Wed, 15 Apr 2015 18:10:43 +0200
Subject: [PATCH] Adding an example that violates an assertion during
 unconstrained simplification.

---
 test/regress/regress0/unconstrained/Makefile.am | 4 +++-
 test/regress/regress0/unconstrained/mult1.smt2  | 8 ++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/unconstrained/mult1.smt2

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)
-- 
2.30.2