fixing bitvector bugs

* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

45 files changed, 154 insertions, 43 deletions

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 07619b965..995ade606 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -29,6 +29,49 @@ SMT_TESTS = \
 	fuzz12.smt \
 	fuzz13.smt \
 	fuzz14.smt \
+	fuzz15.delta01.smt \
+	fuzz16.delta01.smt \
+	fuzz17.delta01.smt \
+	fuzz18.delta01.smt \
+	fuzz18.smt \
+	fuzz19.delta01.smt \
+	fuzz19.smt \
+	fuzz20.delta01.smt \
+	fuzz20.smt \
+	fuzz21.delta01.smt \
+	fuzz21.smt \
+	fuzz22.delta01.smt \
+	fuzz22.smt \
+	fuzz23.delta01.smt \
+	fuzz23.smt \
+	fuzz24.delta01.smt \
+	fuzz24.smt \
+	fuzz25.delta01.smt \
+	fuzz25.smt \
+	fuzz26.delta01.smt \
+	fuzz26.smt \
+	fuzz27.delta01.smt \
+	fuzz27.smt \
+	fuzz28.delta01.smt \
+	fuzz28.smt \
+	fuzz29.delta01.smt \
+	fuzz29.smt \
+	fuzz30.delta01.smt \
+	fuzz30.smt \
+	fuzz31.delta01.smt \
+	fuzz31.smt \
+	fuzz32.delta01.smt \
+	fuzz32.smt \
+	fuzz33.delta01.smt \
+	fuzz33.smt \
+	fuzz34.delta01.smt \
+	fuzz34.smt \
+	fuzz35.delta01.smt \
+	fuzz35.smt \
+	fuzz36.delta01.smt \
+	fuzz36.smt \
+	fuzz37.delta01.smt \
+	fuzz37.smt \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
 
 # Regression tests for SMT2 inputs
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index f58b01bc2..718e8f756 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -68,7 +68,6 @@ TESTS =	\
 	slice-18.smt \
 	slice-19.smt \
 	slice-20.smt \
-	ext_con_004_001_1024.smt \
 	a78test0002.smt \
 	a95test0002.smt \
 	bitvec0.smt \
diff --git a/test/regress/regress0/bv/fuzz15.delta01.smt b/test/regress/regress0/bv/fuzz15.delta01.smt
index f3eb57e17..b3fad3a2b 100644
--- a/test/regress/regress0/bv/fuzz15.delta01.smt
+++ b/test/regress/regress0/bv/fuzz15.delta01.smt
@@ -10,7 +10,7 @@
 :extrafuns ((v0 BitVec[15]))
 :extrafuns ((v14 BitVec[14]))
 :extrafuns ((v19 BitVec[10]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 (sign_extend[2] v11))
 (let (?n2 (sign_extend[6] ?n1))
diff --git a/test/regress/regress0/bv/fuzz16.delta01.smt b/test/regress/regress0/bv/fuzz16.delta01.smt
new file mode 100644
index 000000000..c9fef69de
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz16.delta01.smt
@@ -0,0 +1,69 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v1 BitVec[12]))
+:extrafuns ((v15 BitVec[8]))
+:extrafuns ((v11 BitVec[12]))
+:extrafuns ((v12 BitVec[15]))
+:status unsat
+:formula
+(flet ($n1 true)
+(let (?n2 bv0[12])
+(flet ($n3 (bvslt ?n2 v1))
+(flet ($n4 (not $n3))
+(let (?n5 bv0[1])
+(let (?n6 bv1[1])
+(let (?n7 bv1[12])
+(flet ($n8 (bvult v11 ?n7))
+(let (?n9 (ite $n8 ?n6 ?n5))
+(flet ($n10 (= ?n6 ?n9))
+(let (?n11 (ite $n10 v11 ?n2))
+(let (?n12 (sign_extend[3] ?n11))
+(flet ($n13 (bvult ?n12 v12))
+(let (?n14 (ite $n13 ?n6 ?n5))
+(flet ($n15 (bvult ?n5 ?n14))
+(flet ($n16 (not $n15))
+(let (?n17 bv0[5])
+(let (?n18 (sign_extend[1] v1))
+(let (?n19 (sign_extend[2] ?n18))
+(let (?n20 (bvxnor v12 ?n19))
+(flet ($n21 (bvult ?n19 ?n20))
+(let (?n22 (ite $n21 ?n6 ?n5))
+(let (?n23 (repeat[5] ?n22))
+(flet ($n24 (bvult ?n17 ?n23))
+(let (?n25 bv0[10])
+(let (?n26 bv0[15])
+(flet ($n27 (bvsge ?n20 ?n26))
+(let (?n28 (ite $n27 ?n6 ?n5))
+(let (?n29 (sign_extend[9] ?n28))
+(flet ($n30 (= ?n25 ?n29))
+(let (?n31 bv1[14])
+(flet ($n32 (bvult ?n22 ?n6))
+(let (?n33 (ite $n32 ?n6 ?n5))
+(let (?n34 (zero_extend[13] ?n33))
+(let (?n35 (bvadd ?n31 ?n34))
+(let (?n36 bv0[14])
+(flet ($n37 (bvugt ?n35 ?n36))
+(flet ($n38 false)
+(let (?n39 bv1[15])
+(let (?n40 (zero_extend[4] v15))
+(let (?n41 (bvcomp v11 ?n40))
+(let (?n42 (zero_extend[14] ?n41))
+(flet ($n43 (distinct ?n39 ?n42))
+(let (?n44 (ite $n43 ?n6 ?n5))
+(let (?n45 (sign_extend[11] ?n44))
+(let (?n46 (bvxor v1 ?n45))
+(flet ($n47 (bvsgt ?n2 ?n46))
+(let (?n48 (zero_extend[12] ?n44))
+(let (?n49 bv0[13])
+(flet ($n50 (bvule ?n48 ?n49))
+(flet ($n51 (or $n38 $n47 $n50))
+(flet ($n52 (bvsle ?n2 v1))
+(let (?n53 (ite $n52 ?n6 ?n5))
+(let (?n54 (bvadd ?n6 ?n53))
+(flet ($n55 (bvugt ?n54 ?n5))
+(let (?n56 (ite $n55 ?n6 ?n5))
+(let (?n57 (sign_extend[14] ?n56))
+(flet ($n58 (bvuge ?n57 ?n39))
+(flet ($n59 (and $n4 $n16 $n24 $n30 $n37 $n51 $n58))
+$n59
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/bv/fuzz17.delta01.smt b/test/regress/regress0/bv/fuzz17.delta01.smt
index e4adff5f6..568658e9d 100644
--- a/test/regress/regress0/bv/fuzz17.delta01.smt
+++ b/test/regress/regress0/bv/fuzz17.delta01.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v3 BitVec[11]))
 :extrafuns ((v8 BitVec[9]))
 :extrafuns ((v4 BitVec[14]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv1[16])
diff --git a/test/regress/regress0/bv/fuzz18.delta01.smt b/test/regress/regress0/bv/fuzz18.delta01.smt
index 6622ebc15..87cceb8e8 100644
--- a/test/regress/regress0/bv/fuzz18.delta01.smt
+++ b/test/regress/regress0/bv/fuzz18.delta01.smt
@@ -5,7 +5,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v6 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 (extract[1:1] v2))
diff --git a/test/regress/regress0/bv/fuzz18.smt b/test/regress/regress0/bv/fuzz18.smt
index 71a4eb6f3..aae85a343 100644
--- a/test/regress/regress0/bv/fuzz18.smt
+++ b/test/regress/regress0/bv/fuzz18.smt
@@ -9,7 +9,7 @@
 :extrafuns ((v5 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v7 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (bvcomp v3 v2))
diff --git a/test/regress/regress0/bv/fuzz19.delta01.smt b/test/regress/regress0/bv/fuzz19.delta01.smt
index e6395f1aa..fd044074d 100644
--- a/test/regress/regress0/bv/fuzz19.delta01.smt
+++ b/test/regress/regress0/bv/fuzz19.delta01.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
 :extrafuns ((v5 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (extract[0:0] v2))
diff --git a/test/regress/regress0/bv/fuzz19.smt b/test/regress/regress0/bv/fuzz19.smt
index bcd4dfec0..91bf1e01b 100644
--- a/test/regress/regress0/bv/fuzz19.smt
+++ b/test/regress/regress0/bv/fuzz19.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v5 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (extract[0:0] v2))
diff --git a/test/regress/regress0/bv/fuzz20.delta01.smt b/test/regress/regress0/bv/fuzz20.delta01.smt
index 32c8673d5..66208cf74 100644
--- a/test/regress/regress0/bv/fuzz20.delta01.smt
+++ b/test/regress/regress0/bv/fuzz20.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz20.smt b/test/regress/regress0/bv/fuzz20.smt
index 5cca0878b..b7b493c82 100644
--- a/test/regress/regress0/bv/fuzz20.smt
+++ b/test/regress/regress0/bv/fuzz20.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz21.delta01.smt b/test/regress/regress0/bv/fuzz21.delta01.smt
index 86bcd823c..e74eaff8b 100644
--- a/test/regress/regress0/bv/fuzz21.delta01.smt
+++ b/test/regress/regress0/bv/fuzz21.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvmul v1 v1))
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz21.smt b/test/regress/regress0/bv/fuzz21.smt
index 4af799450..9ad27d844 100644
--- a/test/regress/regress0/bv/fuzz21.smt
+++ b/test/regress/regress0/bv/fuzz21.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz22.delta01.smt b/test/regress/regress0/bv/fuzz22.delta01.smt
index 62b8114d6..a1ef9e444 100644
--- a/test/regress/regress0/bv/fuzz22.delta01.smt
+++ b/test/regress/regress0/bv/fuzz22.delta01.smt
@@ -5,7 +5,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz22.smt b/test/regress/regress0/bv/fuzz22.smt
index fa479ab30..5aad8f7f7 100644
--- a/test/regress/regress0/bv/fuzz22.smt
+++ b/test/regress/regress0/bv/fuzz22.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz23.delta01.smt b/test/regress/regress0/bv/fuzz23.delta01.smt
index e06b0c670..d7aa145b4 100644
--- a/test/regress/regress0/bv/fuzz23.delta01.smt
+++ b/test/regress/regress0/bv/fuzz23.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 (bvnot v1))
diff --git a/test/regress/regress0/bv/fuzz23.smt b/test/regress/regress0/bv/fuzz23.smt
index 5250bac0c..11b207870 100644
--- a/test/regress/regress0/bv/fuzz23.smt
+++ b/test/regress/regress0/bv/fuzz23.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz24.delta01.smt b/test/regress/regress0/bv/fuzz24.delta01.smt
index 9a219175b..84c9db88a 100644
--- a/test/regress/regress0/bv/fuzz24.delta01.smt
+++ b/test/regress/regress0/bv/fuzz24.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvslt v1 ?n1))
diff --git a/test/regress/regress0/bv/fuzz24.smt b/test/regress/regress0/bv/fuzz24.smt
index 0f722108a..a32c1e804 100644
--- a/test/regress/regress0/bv/fuzz24.smt
+++ b/test/regress/regress0/bv/fuzz24.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz25.delta01.smt b/test/regress/regress0/bv/fuzz25.delta01.smt
index 1a26485db..01a7da590 100644
--- a/test/regress/regress0/bv/fuzz25.delta01.smt
+++ b/test/regress/regress0/bv/fuzz25.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvule v0 ?n1))
diff --git a/test/regress/regress0/bv/fuzz25.smt b/test/regress/regress0/bv/fuzz25.smt
index 1193a62e1..a73ddb56b 100644
--- a/test/regress/regress0/bv/fuzz25.smt
+++ b/test/regress/regress0/bv/fuzz25.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz26.delta01.smt b/test/regress/regress0/bv/fuzz26.delta01.smt
index e6467a284..8ea0741dc 100644
--- a/test/regress/regress0/bv/fuzz26.delta01.smt
+++ b/test/regress/regress0/bv/fuzz26.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv0[4])
 (let (?n2 bv14[4])
diff --git a/test/regress/regress0/bv/fuzz26.smt b/test/regress/regress0/bv/fuzz26.smt
index 5a938c9e8..af360df8b 100644
--- a/test/regress/regress0/bv/fuzz26.smt
+++ b/test/regress/regress0/bv/fuzz26.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz27.delta01.smt b/test/regress/regress0/bv/fuzz27.delta01.smt
index 29da5fce3..f7a118b16 100644
--- a/test/regress/regress0/bv/fuzz27.delta01.smt
+++ b/test/regress/regress0/bv/fuzz27.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvslt v0 ?n1))
diff --git a/test/regress/regress0/bv/fuzz27.smt b/test/regress/regress0/bv/fuzz27.smt
index c26632ebc..786a6aa9c 100644
--- a/test/regress/regress0/bv/fuzz27.smt
+++ b/test/regress/regress0/bv/fuzz27.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz28.delta01.smt b/test/regress/regress0/bv/fuzz28.delta01.smt
index 1bfdea909..5f8ca0f84 100644
--- a/test/regress/regress0/bv/fuzz28.delta01.smt
+++ b/test/regress/regress0/bv/fuzz28.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvnot v0))
 (let (?n2 bv1[4])
diff --git a/test/regress/regress0/bv/fuzz28.smt b/test/regress/regress0/bv/fuzz28.smt
index 2c7a71a0f..732017750 100644
--- a/test/regress/regress0/bv/fuzz28.smt
+++ b/test/regress/regress0/bv/fuzz28.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz29.delta01.smt b/test/regress/regress0/bv/fuzz29.delta01.smt
index 31e09808e..ec5e74e1d 100644
--- a/test/regress/regress0/bv/fuzz29.delta01.smt
+++ b/test/regress/regress0/bv/fuzz29.delta01.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (flet ($n2 false)
diff --git a/test/regress/regress0/bv/fuzz29.smt b/test/regress/regress0/bv/fuzz29.smt
index f1275af5c..1a9fb0b73 100644
--- a/test/regress/regress0/bv/fuzz29.smt
+++ b/test/regress/regress0/bv/fuzz29.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz30.delta01.smt b/test/regress/regress0/bv/fuzz30.delta01.smt
index 8f0eecaf0..e99995377 100644
--- a/test/regress/regress0/bv/fuzz30.delta01.smt
+++ b/test/regress/regress0/bv/fuzz30.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvmul v1 v2))
 (let (?n2 (bvneg ?n1))
diff --git a/test/regress/regress0/bv/fuzz30.smt b/test/regress/regress0/bv/fuzz30.smt
index 2fc1669cb..494cde3a3 100644
--- a/test/regress/regress0/bv/fuzz30.smt
+++ b/test/regress/regress0/bv/fuzz30.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz31.delta01.smt b/test/regress/regress0/bv/fuzz31.delta01.smt
index 24ed4fcd4..07f8b4ae3 100644
--- a/test/regress/regress0/bv/fuzz31.delta01.smt
+++ b/test/regress/regress0/bv/fuzz31.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv8[4])
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz31.smt b/test/regress/regress0/bv/fuzz31.smt
index cb64a270e..452e3d2da 100644
--- a/test/regress/regress0/bv/fuzz31.smt
+++ b/test/regress/regress0/bv/fuzz31.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz32.delta01.smt b/test/regress/regress0/bv/fuzz32.delta01.smt
index 0f2b24505..18fed3adf 100644
--- a/test/regress/regress0/bv/fuzz32.delta01.smt
+++ b/test/regress/regress0/bv/fuzz32.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz32.smt b/test/regress/regress0/bv/fuzz32.smt
index 3bf1cbc46..5384eee65 100644
--- a/test/regress/regress0/bv/fuzz32.smt
+++ b/test/regress/regress0/bv/fuzz32.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz33.delta01.smt b/test/regress/regress0/bv/fuzz33.delta01.smt
index 321d7af0d..6d7589ca7 100644
--- a/test/regress/regress0/bv/fuzz33.delta01.smt
+++ b/test/regress/regress0/bv/fuzz33.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv1[4])
diff --git a/test/regress/regress0/bv/fuzz33.smt b/test/regress/regress0/bv/fuzz33.smt
index d7ab6c9a1..b7898b810 100644
--- a/test/regress/regress0/bv/fuzz33.smt
+++ b/test/regress/regress0/bv/fuzz33.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz34.delta01.smt b/test/regress/regress0/bv/fuzz34.delta01.smt
index ab13890bf..2bd289657 100644
--- a/test/regress/regress0/bv/fuzz34.delta01.smt
+++ b/test/regress/regress0/bv/fuzz34.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz34.smt b/test/regress/regress0/bv/fuzz34.smt
index 704702421..200bed99f 100644
--- a/test/regress/regress0/bv/fuzz34.smt
+++ b/test/regress/regress0/bv/fuzz34.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz35.delta01.smt b/test/regress/regress0/bv/fuzz35.delta01.smt
index e44a22c7e..640e44f6f 100644
--- a/test/regress/regress0/bv/fuzz35.delta01.smt
+++ b/test/regress/regress0/bv/fuzz35.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv4[4])
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz35.smt b/test/regress/regress0/bv/fuzz35.smt
index f8f16a8db..73ae721b2 100644
--- a/test/regress/regress0/bv/fuzz35.smt
+++ b/test/regress/regress0/bv/fuzz35.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz36.delta01.smt b/test/regress/regress0/bv/fuzz36.delta01.smt
index 153b46719..65c88add2 100644
--- a/test/regress/regress0/bv/fuzz36.delta01.smt
+++ b/test/regress/regress0/bv/fuzz36.delta01.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (flet ($n2 false)
diff --git a/test/regress/regress0/bv/fuzz36.smt b/test/regress/regress0/bv/fuzz36.smt
index 96924c4a3..b128ef10f 100644
--- a/test/regress/regress0/bv/fuzz36.smt
+++ b/test/regress/regress0/bv/fuzz36.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz37.delta01.smt b/test/regress/regress0/bv/fuzz37.delta01.smt
index 8baaa1101..044894164 100644
--- a/test/regress/regress0/bv/fuzz37.delta01.smt
+++ b/test/regress/regress0/bv/fuzz37.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[4])
 (flet ($n2 (bvugt ?n1 v1))
diff --git a/test/regress/regress0/bv/fuzz37.smt b/test/regress/regress0/bv/fuzz37.smt
index 4bdf0ceee..98fdfda48 100644
--- a/test/regress/regress0/bv/fuzz37.smt
+++ b/test/regress/regress0/bv/fuzz37.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))