4 files changed, 89 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/core/incremental.smt b/test/regress/regress0/bv/core/incremental.smt
new file mode 100644
index 000000000..3a9ff85e0
--- /dev/null
+++ b/test/regress/regress0/bv/core/incremental.smt
@@ -0,0 +1,24 @@
+(benchmark ext_con_004_004_0016.smt
+:logic QF_BV
+:extrafuns ((v4 BitVec[16]))
+:extrafuns ((dummy4 BitVec[1]))
+:extrafuns ((a BitVec[16]))
+:status unknown
+:formula
+(flet ($n1 true)
+(let (?n2 (extract[15:13] a))
+(let (?n3 (extract[15:14] v4))
+(let (?n4 (concat ?n3 dummy4))
+(flet ($n5 (= ?n2 ?n4))
+(let (?n6 (extract[14:12] a))
+(let (?n7 (extract[13:12] v4))
+(let (?n8 (concat dummy4 ?n7))
+(flet ($n9 (= ?n6 ?n8))
+(flet ($n10 (and $n5 $n9))
+(let (?n11 (extract[14:14] v4))
+(let (?n12 (extract[13:13] v4))
+(flet ($n13 (= ?n11 ?n12))
+(flet ($n14 (not $n13))
+(flet ($n15 (and $n1 $n1 $n1 $n10 $n14))
+$n15
+))))))))))))))))
diff --git a/test/regress/regress0/bv/inequality00.smt2 b/test/regress/regress0/bv/inequality00.smt2
new file mode 100644
index 000000000..55e6786af
--- /dev/null
+++ b/test/regress/regress0/bv/inequality00.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/inequality01.smt2 b/test/regress/regress0/bv/inequality01.smt2
new file mode 100644
index 000000000..73a2515df
--- /dev/null
+++ b/test/regress/regress0/bv/inequality01.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v4 v5)
+	 (bvult (_ bv2 16) v2)
+	 (bvult (_ bv5 16) v3)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/inequality02.smt2 b/test/regress/regress0/bv/inequality02.smt2
new file mode 100644
index 000000000..05f11311f
--- /dev/null
+++ b/test/regress/regress0/bv/inequality02.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v0 v1)
+	 (bvult (_ bv5 16) v3)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v5 (_ bv8 16))
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v4 v5)
+	 ))
+(check-sat)
+(exit)