Arithmetic problem that fails --check-models due incompleteness with multiplication.

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index f2b70e280ff6b2d8cd16b739ca56c7a0fe6d4494..a30c99462b6f36cd9a9bea798720a7bf7154c133 100644 (file)
--- 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 (file)
index 0000000..4b1a937
--- /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)