1 files changed, 43 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz14.smt b/test/regress/regress0/bv/fuzz14.smt
new file mode 100644
index 000000000..51a7b7cad
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz14.smt
@@ -0,0 +1,43 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v2 BitVec[13]))
+:extrafuns ((v1 BitVec[2]))
+:status sat
+:formula
+(let (?n1 bv1[1])
+(let (?n2 bv0[2])
+(flet ($n3 (bvsge ?n2 v1))
+(let (?n4 bv0[1])
+(let (?n5 (ite $n3 ?n1 ?n4))
+(flet ($n6 (= ?n1 ?n5))
+(let (?n7 bv0[13])
+(flet ($n8 (bvslt ?n7 v2))
+(let (?n9 (ite $n8 ?n1 ?n4))
+(let (?n10 (bvneg ?n9))
+(let (?n11 (ite $n6 ?n10 ?n9))
+(let (?n12 (zero_extend[12] ?n11))
+(flet ($n13 (= v2 ?n12))
+(flet ($n14 (= ?n1 ?n9))
+(flet ($n15 (and $n13 $n14))
+(flet ($n16 (not $n15))
+(let (?n17 (bvashr v2 v2))
+(let (?n18 (bvshl v2 ?n17))
+(flet ($n19 (= ?n7 ?n18))
+(let (?n20 bv1[13])
+(let (?n21 (bvsub ?n20 v2))
+(flet ($n22 (= ?n17 ?n21))
+(let (?n23 bv1[10])
+(let (?n24 (sign_extend[9] ?n11))
+(flet ($n25 (= ?n23 ?n24))
+(flet ($n26 (if_then_else $n19 $n22 $n25))
+(flet ($n27 (bvult ?n10 ?n1))
+(let (?n28 (ite $n27 ?n1 ?n4))
+(flet ($n29 (= ?n11 ?n28))
+(let (?n30 bv0[4])
+(let (?n31 (sign_extend[3] ?n11))
+(flet ($n32 (= ?n30 ?n31))
+(flet ($n33 (implies $n29 $n32))
+(flet ($n34 (if_then_else $n26 $n33 $n26))
+(flet ($n35 (implies $n16 $n34))
+$n35
+))))))))))))))))))))))))))))))))))))