Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0.

11 files changed, 134 insertions, 1 deletions

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index d0b787f20..f2b70e280 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -25,7 +25,17 @@ TESTS =	\
 	leq.01.smt \
 	miplibtrick.smt \
 	DTP_k2_n35_c175_s15.smt2 \
-	mod.01.smt2
+	mod.01.smt2 \
+	mod.02.smt2 \
+	mod.03.smt2 \
+	div.01.smt2 \
+	div.02.smt2 \
+	div.03.smt2 \
+	div.04.smt2 \
+	div.05.smt2 \
+	div.06.smt2 \
+	div.07.smt2 \
+	div.08.smt2
 #	problem__003.smt2
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/arith/div.01.smt2 b/test/regress/regress0/arith/div.01.smt2
new file mode 100644
index 000000000..d7d587021
--- /dev/null
+++ b/test/regress/regress0/arith/div.01.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+(assert (= n 0))
+(assert (= (div (div n n) n)
+           (div (div (div n n) n) n)))
+(assert (distinct (div (div n n) n)
+                  (div (div (div (div (div n n) n) n) n) n)))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.02.smt2 b/test/regress/regress0/arith/div.02.smt2
new file mode 100644
index 000000000..65dc21549
--- /dev/null
+++ b/test/regress/regress0/arith/div.02.smt2
@@ -0,0 +1,10 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+
+(assert (distinct (div n n) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.03.smt2 b/test/regress/regress0/arith/div.03.smt2
new file mode 100644
index 000000000..17de612bb
--- /dev/null
+++ b/test/regress/regress0/arith/div.03.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Int)
+(declare-fun n () Int)
+
+(assert (> n 0))
+(assert (>= x n))
+(assert (< (div x n) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.04.smt2 b/test/regress/regress0/arith/div.04.smt2
new file mode 100644
index 000000000..c30b1cd2f
--- /dev/null
+++ b/test/regress/regress0/arith/div.04.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (not (=> (= x y) (= (/ x n) (/ y n)))))
+(assert (<= n 0))
+(assert (>= n 0))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2
new file mode 100644
index 000000000..fcc50ec98
--- /dev/null
+++ b/test/regress/regress0/arith/div.05.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y n) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.06.smt2 b/test/regress/regress0/arith/div.06.smt2
new file mode 100644
index 000000000..b33749cc6
--- /dev/null
+++ b/test/regress/regress0/arith/div.06.smt2
@@ -0,0 +1,15 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y n) 1))
+(assert (<= n 0))
+(assert (>= n 0))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.07.smt2 b/test/regress/regress0/arith/div.07.smt2
new file mode 100644
index 000000000..4c45b32c8
--- /dev/null
+++ b/test/regress/regress0/arith/div.07.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y (/ x n)) 1))
+(assert (<= n 0))
+(assert (>= n 0))
+(assert (= x y))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/div.08.smt2 b/test/regress/regress0/arith/div.08.smt2
new file mode 100644
index 000000000..0b0d73ac1
--- /dev/null
+++ b/test/regress/regress0/arith/div.08.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+
+(assert (= (div n n) (div (div n n) n)))
+(assert (distinct (div (div n n) n) (div (div (div n n) n) n)))
+(assert (<= n 0))
+(assert (>= n 0))
+(check-sat)
diff --git a/test/regress/regress0/arith/mod.02.smt2 b/test/regress/regress0/arith/mod.02.smt2
new file mode 100644
index 000000000..75b25c181
--- /dev/null
+++ b/test/regress/regress0/arith/mod.02.smt2
@@ -0,0 +1,11 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+
+(assert (distinct n 0))
+(assert (> (mod n n) 0))
+
+(check-sat)
diff --git a/test/regress/regress0/arith/mod.03.smt2 b/test/regress/regress0/arith/mod.03.smt2
new file mode 100644
index 000000000..760350c89
--- /dev/null
+++ b/test/regress/regress0/arith/mod.03.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+(declare-fun x () Int)
+
+(assert (< (mod x n) 0))
+(assert (< (div x n) 0))
+
+(check-sat)