From: Tim King <taking@cs.nyu.edu>
Date: Fri, 9 Nov 2012 19:58:00 +0000 (+0000)
Subject: Arithmetic problem that fails --check-models due incompleteness with multiplication.
X-Git-Tag: cvc5-1.0.0~7632
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cc7c610a84a29f97a206227d85efbb9a77fda9f;p=cvc5.git

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