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