1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/unsound1.smt2 b/test/regress/regress0/bv/unsound1.smt2
new file mode 100644
index 000000000..60e764537
--- /dev/null
+++ b/test/regress/regress0/bv/unsound1.smt2
@@ -0,0 +1,23 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 4))
+(assert (let ((e1(_ bv0 1)))
+(let ((e2(_ bv11134 16)))
+(let ((e3 (bvadd e2 ((_ sign_extend 12) v0))))
+(let ((e4 (ite (= e2 ((_ sign_extend 12) v0)) (_ bv1 1) (_ bv0 1))))
+(let ((e5 (bvlshr e3 ((_ sign_extend 12) v0))))
+(let ((e6 (bvxnor e2 ((_ zero_extend 12) v0))))
+(let ((e7 (ite (bvult ((_ sign_extend 15) e1) e2) (_ bv1 1) (_ bv0 1))))
+(let ((e8 (bvugt e7 e1)))
+(let ((e9 (bvule ((_ sign_extend 3) e7) v0)))
+(let ((e10 (bvsgt e5 ((_ zero_extend 12) v0))))
+(let ((e11 (= e6 e3)))
+(let ((e12 (bvslt ((_ zero_extend 15) e4) e5)))
+(let ((e13 (bvugt e5 e2)))
+(let ((e14 (ite e10 e8 e10)))
+(let ((e15 (xor e13 e11)))
+(let ((e16 (xor e14 e15)))
+(let ((e17 (ite e9 e12 e16)))
+e17
+))))))))))))))))))
+(check-sat)