1 files changed, 0 insertions, 117 deletions
diff --git a/test/regress/regress0/bv/fuzz18.delta01.smt b/test/regress/regress0/bv/fuzz18.delta01.smt
deleted file mode 100644
index 87cceb8e8..000000000
--- a/test/regress/regress0/bv/fuzz18.delta01.smt
+++ /dev/null
@@ -1,117 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:extrafuns ((v2 BitVec[4]))
-:extrafuns ((v4 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v6 BitVec[4]))
-:status unsat
-:formula
-(let (?n1 bv1[1])
-(let (?n2 (extract[1:1] v2))
-(flet ($n3 (= ?n1 ?n2))
-(let (?n4 bv0[4])
-(let (?n5 bv1[4])
-(let (?n6 (ite $n3 ?n4 ?n5))
-(let (?n7 (bvlshr v2 v4))
-(flet ($n8 (bvule ?n6 ?n7))
-(let (?n9 bv0[1])
-(let (?n10 (ite $n8 ?n1 ?n9))
-(flet ($n11 (distinct ?n1 ?n10))
-(let (?n12 (ite $n11 ?n1 ?n9))
-(let (?n13 (sign_extend[3] ?n12))
-(flet ($n14 (bvuge ?n13 ?n5))
-(flet ($n15 (bvuge v1 v6))
-(let (?n16 (ite $n15 ?n1 ?n9))
-(let (?n17 (sign_extend[3] ?n16))
-(let (?n18 (bvand v1 ?n17))
-(flet ($n19 (bvult ?n18 ?n5))
-(let (?n20 (ite $n19 ?n1 ?n9))
-(flet ($n21 (bvslt ?n1 ?n20))
-(let (?n22 (ite $n21 ?n1 ?n9))
-(let (?n23 (zero_extend[1] ?n22))
-(let (?n24 bv0[2])
-(flet ($n25 (bvsgt ?n23 ?n24))
-(let (?n26 (ite $n25 ?n1 ?n9))
-(let (?n27 (sign_extend[3] ?n26))
-(flet ($n28 (bvsle v2 ?n27))
-(let (?n29 (rotate_left[3] v4))
-(let (?n30 (bvnot ?n29))
-(flet ($n31 (bvslt ?n4 ?n30))
-(let (?n32 (ite $n31 ?n1 ?n9))
-(let (?n33 (zero_extend[3] ?n32))
-(flet ($n34 (bvsge ?n5 ?n33))
-(let (?n35 (bvsub ?n5 ?n30))
-(let (?n36 bv4[4])
-(flet ($n37 (bvule ?n35 ?n36))
-(flet ($n38 false)
-(flet ($n39 (bvult v0 ?n5))
-(let (?n40 (bvshl ?n36 v1))
-(let (?n41 (bvmul v4 ?n18))
-(flet ($n42 (distinct ?n40 ?n41))
-(let (?n43 (ite $n42 ?n1 ?n9))
-(let (?n44 bv1[2])
-(let (?n45 (bvnor v1 ?n30))
-(flet ($n46 (bvuge ?n45 v6))
-(let (?n47 (ite $n46 ?n1 ?n9))
-(let (?n48 (sign_extend[3] ?n47))
-(flet ($n49 (bvult ?n4 ?n48))
-(let (?n50 (ite $n49 ?n1 ?n9))
-(let (?n51 (sign_extend[1] ?n50))
-(flet ($n52 (bvule ?n44 ?n51))
-(let (?n53 (ite $n52 ?n1 ?n9))
-(flet ($n54 (= ?n43 ?n53))
-(let (?n55 (ite $n54 ?n1 ?n9))
-(let (?n56 (sign_extend[3] ?n55))
-(flet ($n57 (bvugt ?n5 ?n56))
-(flet ($n58 (or $n38 $n39 $n57))
-(let (?n59 (sign_extend[3] ?n1))
-(let (?n60 (bvmul v2 ?n36))
-(let (?n61 (bvnor ?n5 ?n60))
-(let (?n62 (bvadd ?n59 ?n61))
-(flet ($n63 (bvsge ?n62 ?n4))
-(flet ($n64 (bvugt ?n59 v2))
-(flet ($n65 (bvsge v6 ?n61))
-(let (?n66 (ite $n65 ?n1 ?n9))
-(let (?n67 (bvshl v1 v0))
-(flet ($n68 (bvuge ?n4 ?n40))
-(let (?n69 (ite $n68 ?n1 ?n9))
-(let (?n70 (bvxnor ?n9 ?n69))
-(let (?n71 (sign_extend[3] ?n70))
-(flet ($n72 (bvuge v6 ?n71))
-(let (?n73 (ite $n72 ?n1 ?n9))
-(let (?n74 (zero_extend[3] ?n73))
-(flet ($n75 (bvsle ?n67 ?n74))
-(let (?n76 (ite $n75 ?n1 ?n9))
-(flet ($n77 (bvugt ?n66 ?n76))
-(flet ($n78 (or $n38 $n64 $n77))
-(flet ($n79 (bvult ?n4 ?n18))
-(let (?n80 (ite $n79 ?n1 ?n9))
-(flet ($n81 (bvule ?n1 ?n80))
-(flet ($n82 (not $n81))
-(let (?n83 (sign_extend[1] ?n66))
-(flet ($n84 (= ?n24 ?n83))
-(flet ($n85 (or $n38 $n82 $n84))
-(flet ($n86 (bvuge ?n29 ?n62))
-(flet ($n87 (bvsgt ?n45 ?n4))
-(let (?n88 (ite $n87 ?n1 ?n9))
-(flet ($n89 (bvsge ?n10 ?n88))
-(flet ($n90 (bvsgt ?n4 v0))
-(let (?n91 (ite $n90 ?n1 ?n9))
-(let (?n92 (zero_extend[3] ?n91))
-(flet ($n93 (bvsgt v0 ?n92))
-(flet ($n94 (or $n38 $n89 $n93))
-(let (?n95 (bvcomp ?n4 ?n7))
-(let (?n96 (sign_extend[3] ?n95))
-(flet ($n97 (bvugt ?n96 ?n5))
-(let (?n98 (ite $n97 ?n1 ?n9))
-(flet ($n99 (bvsgt ?n98 ?n1))
-(flet ($n100 (bvule ?n45 ?n5))
-(let (?n101 (ite $n100 ?n1 ?n9))
-(flet ($n102 (bvslt ?n101 ?n9))
-(flet ($n103 (bvsge v2 ?n59))
-(let (?n104 (ite $n103 ?n1 ?n9))
-(flet ($n105 (bvugt ?n104 ?n9))
-(flet ($n106 (and $n14 $n28 $n34 $n37 $n58 $n63 $n78 $n85 $n86 $n94 $n99 $n102 $n105))
-$n106
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))