Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

52 files changed, 1275 insertions, 0 deletions

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
new file mode 100644
index 000000000..241b78848
--- /dev/null
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -0,0 +1,78 @@
+BINARY = cvc4
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
+else
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	arith2.smt2 \
+	arith3.smt2 \
+	arith4.smt2 \
+	arith5.smt2 \
+	arith6.smt2 \
+	arith7.smt2 \
+	arith.smt2 \
+	array1.smt2 \
+	bvbool2.smt2 \
+	bvbool3.smt2 \
+	bvbool.smt2 \
+	bvcmp.smt2 \
+	bvconcat2.smt2 \
+	bvconcat.smt2 \
+	bvdiv2.smt2 \
+	bvdiv.smt2 \
+	bvext.smt2 \
+	bvite.smt2 \
+	bvmul2.smt2 \
+	bvmul3.smt2 \
+	bvmul.smt2 \
+	bvnot.smt2 \
+	bvsle2.smt2 \
+	bvsle3.smt2 \
+	bvsle4.smt2 \
+	bvsle5.smt2 \
+	bvsle.smt2 \
+	bvslt2.smt2 \
+	bvslt3.smt2 \
+	bvslt4.smt2 \
+	bvslt5.smt2 \
+	bvslt.smt2 \
+	bvule2.smt2 \
+	bvule3.smt2 \
+	bvule4.smt2 \
+	bvule5.smt2 \
+	bvule.smt2 \
+	bvult2.smt2 \
+	bvult3.smt2 \
+	bvult4.smt2 \
+	bvult5.smt2 \
+	bvult.smt2 \
+	geq.smt2 \
+	gt.smt2 \
+	leq.smt2 \
+	lt.smt2 \
+	uf1.smt2 \
+	uf2.smt2 \
+	xor.smt2
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/unconstrained/arith.smt2 b/test/regress/regress0/unconstrained/arith.smt2
new file mode 100644
index 000000000..dc2b27414
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (< v2 100))
+(assert (not (= (a2 (- (+ v1 5) v2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith2.smt2 b/test/regress/regress0/unconstrained/arith2.smt2
new file mode 100644
index 000000000..f9e829e45
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith2.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Real)
+(assert (= (+ v1 v2) v3))
+(assert (< v3 v2))
+(assert (> v3 (- v2 1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith3.smt2 b/test/regress/regress0/unconstrained/arith3.smt2
new file mode 100644
index 000000000..83634a50a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith3.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Int)
+(declare-fun v4 () Int)
+(assert (= (* v1 v2) v3))
+(assert (< v3 v4))
+(assert (> v3 (- v4 1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith4.smt2 b/test/regress/regress0/unconstrained/arith4.smt2
new file mode 100644
index 000000000..8cb825a8d
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith4.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun v3 () Int)
+(declare-fun v4 () Int)
+(declare-fun v5 () Real)
+(assert (= (* v1 v2) (+ (* v3 v4) v5)))
+(assert (< v5 1))
+(assert (> v5 0))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith5.smt2 b/test/regress/regress0/unconstrained/arith5.smt2
new file mode 100644
index 000000000..de1e305bc
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith5.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Real)
+(declare-fun a2 (Real) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (* 2 v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith6.smt2 b/test/regress/regress0/unconstrained/arith6.smt2
new file mode 100644
index 000000000..05653415f
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith6.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Real)
+(declare-fun a2 (Real) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (/ v1 2)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/arith7.smt2 b/test/regress/regress0/unconstrained/arith7.smt2
new file mode 100644
index 000000000..6cc063ca4
--- /dev/null
+++ b/test/regress/regress0/unconstrained/arith7.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Real)
+(assert (= (/ v1 2) v2))
+(assert (< v2 (/ 1 2)))
+(assert (> v2 0))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/array1.smt2 b/test/regress/regress0/unconstrained/array1.smt2
new file mode 100644
index 000000000..82f084e87
--- /dev/null
+++ b/test/regress/regress0/unconstrained/array1.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun a2 () (Array (_ BitVec 16) (_ BitVec 1024)))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (select a2 v1) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvbool.smt2 b/test/regress/regress0/unconstrained/bvbool.smt2
new file mode 100644
index 000000000..0dded2a2f
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvbool2.smt2 b/test/regress/regress0/unconstrained/bvbool2.smt2
new file mode 100644
index 000000000..949096224
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool2.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (= (bvand x0 x1) ((_ extract 9 0) v3)))
+(assert (= x1 (_ bv0 10)))
+(assert (= v3 (_ bv1 1024)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2
new file mode 100644
index 000000000..6f72246f0
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool3.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or p1 p1) (and (= (bvnor (bvnand (bvor x1 x1) (bvand x0 x0)) x3) ((_ extract 9 0) v3)) p1))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvbool3.smt3 b/test/regress/regress0/unconstrained/bvbool3.smt3
new file mode 100644
index 000000000..7c9362672
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvbool3.smt3
@@ -0,0 +1,37 @@
+(set-logic QF_AUFBVLIA)
+(set-info :source |
+This benchmark demonstrates the need for propagating unconstrained arrays
+and bit-vectors.
+
+Contributed by Robert Brummayer (robert.brummayer@gmail.com)
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun p1 () Bool)
+(declare-fun p2 () Bool)
+(declare-fun p3 () Bool)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvcmp.smt2 b/test/regress/regress0/unconstrained/bvcmp.smt2
new file mode 100644
index 000000000..ba7316324
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvcmp.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= (bvcomp v1 (_ bv0 1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvconcat.smt2 b/test/regress/regress0/unconstrained/bvconcat.smt2
new file mode 100644
index 000000000..e2941b34a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvconcat.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (concat (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 19 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvconcat2.smt2 b/test/regress/regress0/unconstrained/bvconcat2.smt2
new file mode 100644
index 000000000..aa901b9b0
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvconcat2.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (concat x0 x0) (_ bv1 20)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvdiv.smt2 b/test/regress/regress0/unconstrained/bvdiv.smt2
new file mode 100644
index 000000000..d3cadf6c8
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvdiv.smt2
@@ -0,0 +1,33 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvshl (bvlshr (bvashr (bvudiv x0 x1) (bvurem x2 x3)) (bvudiv x4 x5)) (bvurem x6 x7)) ((_ extract 9 0) v4))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2
new file mode 100644
index 000000000..6314701b3
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvdiv2.smt2
@@ -0,0 +1,26 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (= (bvudiv x0 x0) (_ bv1 10))
+ )
+)
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvext.smt2 b/test/regress/regress0/unconstrained/bvext.smt2
new file mode 100644
index 000000000..56289e245
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvext.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= ((_ extract 3 0) v1) ((_ extract 3 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvite.smt2 b/test/regress/regress0/unconstrained/bvite.smt2
new file mode 100644
index 000000000..9e1ecc193
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvite.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (ite (= x0 ((_ extract 9 0) v3)) ((_ extract 0 0) v4) (bvnot ((_
+     extract 0 0) v4))) ((_ extract 0 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvmul.smt2 b/test/regress/regress0/unconstrained/bvmul.smt2
new file mode 100644
index 000000000..fc56695f5
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvmul x0 x1) ((_ extract 9 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvmul2.smt2 b/test/regress/regress0/unconstrained/bvmul2.smt2
new file mode 100644
index 000000000..89e4ff569
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul2.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun x8 () (_ BitVec 10))
+(declare-fun x9 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (bvmul x0 (_ bv2 10)) (_ bv1 10)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvmul3.smt2 b/test/regress/regress0/unconstrained/bvmul3.smt2
new file mode 100644
index 000000000..ea67a1b5a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvmul3.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (bvmul x0 (_ bv15 10)) ((_ extract 9 0) v3))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvnot.smt2 b/test/regress/regress0/unconstrained/bvnot.smt2
new file mode 100644
index 000000000..22fc7e7d2
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvnot.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (= (bvnot (bvneg v1)) ((_ extract 0 0) v3)) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvsle.smt2 b/test/regress/regress0/unconstrained/bvsle.smt2
new file mode 100644
index 000000000..702f9d7a0
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvsle2.smt2 b/test/regress/regress0/unconstrained/bvsle2.smt2
new file mode 100644
index 000000000..b797fa4e8
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv513 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvsle3.smt2 b/test/regress/regress0/unconstrained/bvsle3.smt2
new file mode 100644
index 000000000..4d897830c
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvslt x0 (_ bv513 10)))
+(assert (not (bvsle x0 x1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvsle4.smt2 b/test/regress/regress0/unconstrained/bvsle4.smt2
new file mode 100644
index 000000000..8927a5f2e
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv510 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvsle x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvsle5.smt2 b/test/regress/regress0/unconstrained/bvsle5.smt2
new file mode 100644
index 000000000..1aceacbe3
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvsle5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvsgt x1 (_ bv510 10)))
+(assert (not (bvsle x0 x1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvslt.smt2 b/test/regress/regress0/unconstrained/bvslt.smt2
new file mode 100644
index 000000000..f98375653
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvslt2.smt2 b/test/regress/regress0/unconstrained/bvslt2.smt2
new file mode 100644
index 000000000..e56500ad2
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv510 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvslt3.smt2 b/test/regress/regress0/unconstrained/bvslt3.smt2
new file mode 100644
index 000000000..a4af152f1
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvsgt x0 (_ bv510 10)))
+(assert (bvslt x0 x1))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvslt4.smt2 b/test/regress/regress0/unconstrained/bvslt4.smt2
new file mode 100644
index 000000000..d702b6d1a
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv513 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvslt x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvslt5.smt2 b/test/regress/regress0/unconstrained/bvslt5.smt2
new file mode 100644
index 000000000..f4b6a7a63
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvslt5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvslt x1 (_ bv513 10)))
+(assert (bvslt x0 x1))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvule.smt2 b/test/regress/regress0/unconstrained/bvule.smt2
new file mode 100644
index 000000000..cbbb4cc6e
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvule2.smt2 b/test/regress/regress0/unconstrained/bvule2.smt2
new file mode 100644
index 000000000..0e6f5916b
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv1 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvule3.smt2 b/test/regress/regress0/unconstrained/bvule3.smt2
new file mode 100644
index 000000000..11e3a9877
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvult x0 (_ bv1 10)))
+(assert (not (bvule x0 x1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvule4.smt2 b/test/regress/regress0/unconstrained/bvule4.smt2
new file mode 100644
index 000000000..b8d978b71
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv1022 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvule x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvule5.smt2 b/test/regress/regress0/unconstrained/bvule5.smt2
new file mode 100644
index 000000000..cd927d0c6
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvule5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvugt x1 (_ bv1022 10)))
+(assert (not (bvule x0 x1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvult.smt2 b/test/regress/regress0/unconstrained/bvult.smt2
new file mode 100644
index 000000000..fb94994b4
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvult2.smt2 b/test/regress/regress0/unconstrained/bvult2.smt2
new file mode 100644
index 000000000..3fb4a0d23
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult2.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x0 (_ bv1022 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvult3.smt2 b/test/regress/regress0/unconstrained/bvult3.smt2
new file mode 100644
index 000000000..b11ab9da3
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvugt x0 (_ bv1022 10)))
+(assert (bvult x0 x1))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvult4.smt2 b/test/regress/regress0/unconstrained/bvult4.smt2
new file mode 100644
index 000000000..8170ec280
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult4.smt2
@@ -0,0 +1,32 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= x1 (_ bv1 10)))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (bvult x0 x1)
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/bvult5.smt2 b/test/regress/regress0/unconstrained/bvult5.smt2
new file mode 100644
index 000000000..545bcbf64
--- /dev/null
+++ b/test/regress/regress0/unconstrained/bvult5.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (bvult x1 (_ bv1 10)))
+(assert (bvult x0 x1))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/files b/test/regress/regress0/unconstrained/files
new file mode 100644
index 000000000..8a0f48889
--- /dev/null
+++ b/test/regress/regress0/unconstrained/files
@@ -0,0 +1,49 @@
+arith2.smt2
+arith3.smt2
+arith4.smt2
+arith5.smt2
+arith6.smt2
+arith7.smt2
+arith.smt2
+array1.smt2
+bvbool2.smt2
+bvbool3.smt2
+bvbool.smt2
+bvcmp.smt2
+bvconcat2.smt2
+bvconcat.smt2
+bvdiv2.smt2
+bvdiv.smt2
+bvext.smt2
+bvite.smt2
+bvmul2.smt2
+bvmul3.smt2
+bvmul.smt2
+bvnot.smt2
+bvsle2.smt2
+bvsle3.smt2
+bvsle4.smt2
+bvsle5.smt2
+bvsle.smt2
+bvslt2.smt2
+bvslt3.smt2
+bvslt4.smt2
+bvslt5.smt2
+bvslt.smt2
+bvule2.smt2
+bvule3.smt2
+bvule4.smt2
+bvule5.smt2
+bvule.smt2
+bvult2.smt2
+bvult3.smt2
+bvult4.smt2
+bvult5.smt2
+bvult.smt2
+geq.smt2
+gt.smt2
+leq.smt2
+lt.smt2
+uf1.smt2
+uf2.smt2
+xor.smt2
diff --git a/test/regress/regress0/unconstrained/geq.smt2 b/test/regress/regress0/unconstrained/geq.smt2
new file mode 100644
index 000000000..818bb55b3
--- /dev/null
+++ b/test/regress/regress0/unconstrained/geq.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (>= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/gt.smt2 b/test/regress/regress0/unconstrained/gt.smt2
new file mode 100644
index 000000000..76b119e42
--- /dev/null
+++ b/test/regress/regress0/unconstrained/gt.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (> v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/leq.smt2 b/test/regress/regress0/unconstrained/leq.smt2
new file mode 100644
index 000000000..6c03fc254
--- /dev/null
+++ b/test/regress/regress0/unconstrained/leq.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (<= v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/lt.smt2 b/test/regress/regress0/unconstrained/lt.smt2
new file mode 100644
index 000000000..637a6407f
--- /dev/null
+++ b/test/regress/regress0/unconstrained/lt.smt2
@@ -0,0 +1,13 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (ite (< v1 5) v2 6)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/uf1.smt2 b/test/regress/regress0/unconstrained/uf1.smt2
new file mode 100644
index 000000000..0b2a95f49
--- /dev/null
+++ b/test/regress/regress0/unconstrained/uf1.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v1 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (not (= (a2 (- v1)) (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/uf2.smt2 b/test/regress/regress0/unconstrained/uf2.smt2
new file mode 100644
index 000000000..0aa1617eb
--- /dev/null
+++ b/test/regress/regress0/unconstrained/uf2.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v1 () (_ BitVec 1))
+(declare-fun a2 ((_ BitVec 1)) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert (= (a2 (_ bv0 1)) v3))
+(assert (= (a2 (_ bv1 1)) v3))
+(assert (not (= (a2 v1) v3)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/unconstrained/xor.smt2 b/test/regress/regress0/unconstrained/xor.smt2
new file mode 100644
index 000000000..4089bb5dc
--- /dev/null
+++ b/test/regress/regress0/unconstrained/xor.smt2
@@ -0,0 +1,33 @@
+(set-logic QF_AUFBVLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () (_ BitVec 10))
+(declare-fun x1 () (_ BitVec 10))
+(declare-fun x2 () (_ BitVec 10))
+(declare-fun x3 () (_ BitVec 10))
+(declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
+(declare-fun x6 () (_ BitVec 10))
+(declare-fun x7 () (_ BitVec 10))
+(declare-fun v2 () Int)
+(declare-fun a2 (Int) (_ BitVec 1024))
+(declare-fun v3 () (_ BitVec 1024))
+(declare-fun v4 () (_ BitVec 1024))
+(declare-fun v5 () (_ BitVec 1024))
+(assert
+ (not
+  (=
+   (a2
+    (ite 
+     (= (xor (= (bvxor (bvxnor (bvadd (bvsub x0 ((_ extract 9 0) v3)) ((_ extract
+     9 0) v4)) ((_ extract 9 0) v5)) ((_ extract 19 10) v3)) ((_ extract 19 10)
+     v4)) (= v3 v4)) (= v4 v5))
+     v2
+     6)
+    )
+   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
+  )
+ )
+(check-sat)
+(exit)