1 files changed, 0 insertions, 43 deletions
diff --git a/test/regress/regress0/bv/fuzz14.smt b/test/regress/regress0/bv/fuzz14.smt
deleted file mode 100644
index 51a7b7cad..000000000
--- a/test/regress/regress0/bv/fuzz14.smt
+++ /dev/null
@@ -1,43 +0,0 @@
-(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
-))))))))))))))))))))))))))))))))))))