1 files changed, 0 insertions, 90 deletions
diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt
deleted file mode 100644
index d8c0b8480..000000000
--- a/test/regress/regress0/aufbv/fuzz13.smt
+++ /dev/null
@@ -1,90 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AUFBV
-:status sat
-:extrafuns ((v0 BitVec[9]))
-:extrafuns ((v1 BitVec[14]))
-:extrafuns ((a2 Array[2:5]))
-:extrafuns ((a3 Array[8:5]))
-:formula
-(let (?e4 bv712[10])
-(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1]))
-(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1))
-(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6)))
-(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1)))
-(let (?e9 (select ?e8 (extract[12:11] v1)))
-(let (?e10 (select a2 (extract[2:1] ?e4)))
-(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10))
-(let (?e12 (select ?e11 (extract[1:0] ?e10)))
-(let (?e13 (select a2 (extract[3:2] ?e9)))
-(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1]))
-(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13)))
-(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1]))
-(let (?e17 (extract[0:0] ?e5))
-(let (?e18 (zero_extend[0] ?e6))
-(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1))
-(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6))
-(flet ($e21 (bvugt v1 (zero_extend[9] ?e12)))
-(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14)))
-(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10)))
-(flet ($e24 (bvugt ?e19 v1))
-(flet ($e25 (bvult (sign_extend[4] ?e12) v0))
-(flet ($e26 (= (sign_extend[4] ?e15) v1))
-(flet ($e27 (= ?e19 (sign_extend[9] ?e12)))
-(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6))
-(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5)))
-(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9))
-(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12))
-(flet ($e32 (bvslt ?e10 ?e12))
-(flet ($e33 (distinct ?e6 ?e18))
-(flet ($e34 (bvsge (sign_extend[4] ?e12) v0))
-(flet ($e35 (bvsge ?e6 (zero_extend[5] v0)))
-(flet ($e36 (distinct v0 (sign_extend[4] ?e13)))
-(flet ($e37 (= ?e18 (sign_extend[5] v0)))
-(flet ($e38 (bvugt ?e16 ?e5))
-(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16)))
-(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19))
-(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5)))
-(flet ($e42 (bvslt (zero_extend[4] ?e12) v0))
-(flet ($e43 (bvugt ?e14 ?e17))
-(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13))
-(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12))
-(flet ($e46 (bvsge ?e19 ?e6))
-(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14)))
-(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4)))
-(flet ($e49 (and $e22 $e30))
-(flet ($e50 (or $e38 $e29))
-(flet ($e51 (xor $e41 $e34))
-(flet ($e52 (iff $e21 $e48))
-(flet ($e53 (iff $e46 $e23))
-(flet ($e54 (iff $e33 $e44))
-(flet ($e55 (and $e24 $e43))
-(flet ($e56 (implies $e32 $e31))
-(flet ($e57 (or $e56 $e47))
-(flet ($e58 (xor $e50 $e40))
-(flet ($e59 (or $e57 $e45))
-(flet ($e60 (iff $e42 $e59))
-(flet ($e61 (or $e35 $e36))
-(flet ($e62 (if_then_else $e51 $e60 $e25))
-(flet ($e63 (or $e55 $e54))
-(flet ($e64 (xor $e53 $e39))
-(flet ($e65 (and $e63 $e63))
-(flet ($e66 (or $e61 $e28))
-(flet ($e67 (and $e27 $e27))
-(flet ($e68 (or $e26 $e26))
-(flet ($e69 (or $e65 $e49))
-(flet ($e70 (xor $e58 $e62))
-(flet ($e71 (implies $e68 $e37))
-(flet ($e72 (if_then_else $e52 $e52 $e70))
-(flet ($e73 (implies $e66 $e67))
-(flet ($e74 (xor $e64 $e71))
-(flet ($e75 (and $e73 $e73))
-(flet ($e76 (implies $e72 $e69))
-(flet ($e77 (xor $e76 $e75))
-(flet ($e78 (iff $e77 $e74))
-(flet ($e79 (and $e78 (not (= v1 bv0[14]))))
-(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14])))))
-(flet ($e81 (and $e80 (not (= ?e6 bv0[14]))))
-(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14])))))
-$e82
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-