3 files changed, 38 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 5d3fe371e..dbd9547a9 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -20,6 +20,7 @@ MAKEFLAGS = -k
 # Regression tests for SMT inputs
 SMT_TESTS = \
 	fuzz01.smt \
+	fuzz02.delta01.smt \
 	fuzz02.smt \
 	fuzz03.smt \
 	fuzz04.smt \
diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2
new file mode 100644
index 000000000..1feb32c7f
--- /dev/null
+++ b/test/regress/regress0/bv/decision-weight00.smt2
@@ -0,0 +1,19 @@
+(set-option :produce-models true)
+(set-logic QF_BV)
+(set-info :source |
+ Patrice Godefroid, SAGE (systematic dynamic test generation)
+ For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unknown)
+(declare-fun x () (_ BitVec 32))
+(declare-fun y () (_ BitVec 32))
+(declare-fun z () (_ BitVec 4))
+(assert (or
+		(= x (bvmul x y))
+		(and (= x y)
+		     (not (= ((_ extract 2 2) x) ((_ extract 2 2) z))))
+		))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/fuzz02.delta01.smt b/test/regress/regress0/bv/fuzz02.delta01.smt
new file mode 100644
index 000000000..1ef924ef1
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz02.delta01.smt
@@ -0,0 +1,18 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v2 BitVec[9]))
+:status unsat
+:formula
+(let (?n1 bv0[2])
+(let (?n2 bv0[6])
+(flet ($n3 (bvult v2 v2))
+(let (?n4 bv1[1])
+(let (?n5 bv0[1])
+(let (?n6 (ite $n3 ?n4 ?n5))
+(let (?n7 (concat ?n2 ?n6))
+(let (?n8 bv0[7])
+(let (?n9 (bvcomp ?n7 ?n8))
+(let (?n10 (zero_extend[1] ?n9))
+(flet ($n11 (= ?n1 ?n10))
+$n11
+))))))))))))