From 3cc7c610a84a29f97a206227d85efbb9a77fda9f Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 9 Nov 2012 19:58:00 +0000
Subject: [PATCH] Arithmetic problem that fails --check-models due
 incompleteness with multiplication.

---
 test/regress/regress0/arith/Makefile.am  |  3 ++-
 test/regress/regress0/arith/mult.01.smt2 | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/arith/mult.01.smt2

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index f2b70e280..a30c99462 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -35,7 +35,8 @@ TESTS =	\
 	div.05.smt2 \
 	div.06.smt2 \
 	div.07.smt2 \
-	div.08.smt2
+	div.08.smt2 \
+	mult.01.smt2
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/arith/mult.01.smt2 b/test/regress/regress0/arith/mult.01.smt2
new file mode 100644
index 000000000..4b1a937f6
--- /dev/null
+++ b/test/regress/regress0/arith/mult.01.smt2
@@ -0,0 +1,17 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Real)
+(declare-fun x () Real)
+
+; This example is to exercise the model builder with unknown results
+
+(assert (>= n 1))
+(assert (<= n 1))
+(assert (<= x 1))
+(assert (>= x 1))
+(assert (not (= (* x n) 1)))
+
+(check-sat)
-- 
2.30.2