1 files changed, 0 insertions, 133 deletions
diff --git a/test/regress/regress0/aufbv/bug348.smt b/test/regress/regress0/aufbv/bug348.smt
deleted file mode 100644
index 46172eba9..000000000
--- a/test/regress/regress0/aufbv/bug348.smt
+++ /dev/null
@@ -1,133 +0,0 @@
-(benchmark B_
-:logic QF_AUFBV
-:extrafuns ((start2 BitVec[32]))
-:extrafuns ((start1 BitVec[32]))
-:extrafuns ((a1 Array[32:8]))
-:status unsat
-:formula
-(let (?n1 bv0[1])
-(let (?n2 bv0[8])
-(let (?n3 (store a1 start1 ?n2))
-(let (?n4 bv3[32])
-(let (?n5 (bvadd ?n4 start1))
-(let (?n6 (store ?n3 ?n5 ?n2))
-(let (?n7 bv0[32])
-(let (?n8 (select ?n6 ?n7))
-(let (?n9 (bvnot ?n8))
-(let (?n10 (select ?n6 ?n7))
-(let (?n11 (bvnot ?n10))
-(let (?n12 (bvand ?n9 ?n11))
-(let (?n13 (bvnot ?n12))
-(let (?n14 (bvand ?n8 ?n10))
-(let (?n15 (bvnot ?n14))
-(let (?n16 (bvand ?n13 ?n15))
-(let (?n17 (bvnot ?n16))
-(let (?n18 (bvand ?n9 ?n17))
-(let (?n19 (bvnot ?n18))
-(let (?n20 (bvand ?n8 ?n16))
-(let (?n21 (bvnot ?n20))
-(let (?n22 (bvand ?n19 ?n21))
-(let (?n23 (store ?n6 ?n7 ?n22))
-(let (?n24 (bvnot ?n22))
-(let (?n25 (bvand ?n17 ?n24))
-(let (?n26 (bvnot ?n25))
-(let (?n27 (bvand ?n16 ?n22))
-(let (?n28 (bvnot ?n27))
-(let (?n29 (bvand ?n26 ?n28))
-(let (?n30 (store ?n23 ?n7 ?n29))
-(let (?n31 (bvadd ?n4 start2))
-(let (?n32 (select ?n30 ?n31))
-(let (?n33 (bvnot ?n32))
-(let (?n34 (select ?n30 start2))
-(let (?n35 (bvnot ?n34))
-(let (?n36 (bvand ?n33 ?n35))
-(let (?n37 (bvnot ?n36))
-(let (?n38 (bvand ?n32 ?n34))
-(let (?n39 (bvnot ?n38))
-(let (?n40 (bvand ?n37 ?n39))
-(let (?n41 (bvnot ?n40))
-(let (?n42 (bvand ?n33 ?n41))
-(let (?n43 (bvnot ?n42))
-(let (?n44 (bvand ?n32 ?n40))
-(let (?n45 (bvnot ?n44))
-(let (?n46 (bvand ?n43 ?n45))
-(let (?n47 (store ?n30 ?n31 ?n46))
-(let (?n48 (bvnot ?n46))
-(let (?n49 (bvand ?n41 ?n48))
-(let (?n50 (bvnot ?n49))
-(let (?n51 (bvand ?n40 ?n46))
-(let (?n52 (bvnot ?n51))
-(let (?n53 (bvand ?n50 ?n52))
-(let (?n54 (store ?n47 start2 ?n53))
-(let (?n55 (select ?n54 ?n7))
-(let (?n56 (bvnot ?n55))
-(let (?n57 (select ?n54 start2))
-(let (?n58 (bvnot ?n57))
-(let (?n59 (bvand ?n56 ?n58))
-(let (?n60 (bvnot ?n59))
-(let (?n61 (bvand ?n55 ?n57))
-(let (?n62 (bvnot ?n61))
-(let (?n63 (bvand ?n60 ?n62))
-(let (?n64 (bvnot ?n63))
-(let (?n65 (bvand ?n56 ?n64))
-(let (?n66 (bvnot ?n65))
-(let (?n67 (bvand ?n55 ?n63))
-(let (?n68 (bvnot ?n67))
-(let (?n69 (bvand ?n66 ?n68))
-(let (?n70 (store ?n54 ?n7 ?n69))
-(let (?n71 (bvnot ?n69))
-(let (?n72 (bvand ?n64 ?n71))
-(let (?n73 (bvnot ?n72))
-(let (?n74 (bvand ?n63 ?n69))
-(let (?n75 (bvnot ?n74))
-(let (?n76 (bvand ?n73 ?n75))
-(let (?n77 (store ?n70 start2 ?n76))
-(let (?n78 (select ?n77 ?n7))
-(let (?n79 (bvnot ?n78))
-(let (?n80 (select ?n77 ?n7))
-(let (?n81 (bvnot ?n80))
-(let (?n82 (bvand ?n79 ?n81))
-(let (?n83 (bvnot ?n82))
-(let (?n84 (bvand ?n78 ?n80))
-(let (?n85 (bvnot ?n84))
-(let (?n86 (bvand ?n83 ?n85))
-(let (?n87 (bvnot ?n86))
-(let (?n88 (bvand ?n79 ?n87))
-(let (?n89 (bvnot ?n88))
-(let (?n90 (bvand ?n78 ?n86))
-(let (?n91 (bvnot ?n90))
-(let (?n92 (bvand ?n89 ?n91))
-(let (?n93 (store ?n77 ?n7 ?n92))
-(let (?n94 (bvnot ?n92))
-(let (?n95 (bvand ?n87 ?n94))
-(let (?n96 (bvnot ?n95))
-(let (?n97 (bvand ?n86 ?n92))
-(let (?n98 (bvnot ?n97))
-(let (?n99 (bvand ?n96 ?n98))
-(let (?n100 (store ?n93 ?n7 ?n99))
-(let (?n101 (store a1 ?n5 ?n2))
-(let (?n102 (store ?n101 start1 ?n2))
-(let (?n103 (select ?n102 ?n7))
-(let (?n104 (store ?n102 ?n7 ?n103))
-(let (?n105 (select ?n102 ?n7))
-(let (?n106 (store ?n104 ?n7 ?n105))
-(let (?n107 (select ?n106 start2))
-(let (?n108 (store ?n106 ?n31 ?n107))
-(let (?n109 (select ?n106 ?n31))
-(let (?n110 (store ?n108 start2 ?n109))
-(let (?n111 (select ?n110 start2))
-(let (?n112 (store ?n110 ?n7 ?n111))
-(let (?n113 (select ?n110 ?n7))
-(let (?n114 (store ?n112 start2 ?n113))
-(let (?n115 (select ?n114 ?n7))
-(let (?n116 (store ?n114 ?n7 ?n115))
-(let (?n117 (select ?n114 ?n7))
-(let (?n118 (store ?n116 ?n7 ?n117))
-(flet ($n119 (= ?n100 ?n118))
-(let (?n120 bv1[1])
-(let (?n121 (ite $n119 ?n120 ?n1))
-(let (?n122 (bvnot ?n121))
-(flet ($n123 (= ?n1 ?n122))
-(flet ($n124 (not $n123))
-$n124
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))