1 files changed, 0 insertions, 122 deletions
diff --git a/test/regress/regress0/bv/fuzz02.smt b/test/regress/regress0/bv/fuzz02.smt
deleted file mode 100644
index 41b616ef0..000000000
--- a/test/regress/regress0/bv/fuzz02.smt
+++ /dev/null
@@ -1,122 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status sat
-:extrafuns ((v0 BitVec[3]))
-:extrafuns ((v1 BitVec[12]))
-:extrafuns ((v2 BitVec[9]))
-:formula
-(let (?e3 bv10[9])
-(let (?e4 (extract[6:6] ?e3))
-(let (?e5 (ite (bvult v2 v2) bv1[1] bv0[1]))
-(let (?e6 (ite (bvsgt ?e4 ?e4) bv1[1] bv0[1]))
-(let (?e7 (sign_extend[5] ?e6))
-(let (?e8 (concat ?e7 ?e5))
-(let (?e9 (bvcomp ?e8 (zero_extend[1] ?e7)))
-(let (?e10 (ite (bvule ?e7 (zero_extend[5] ?e9)) bv1[1] bv0[1]))
-(let (?e11 (bvadd (sign_extend[2] ?e10) v0))
-(let (?e12 (extract[1:0] v0))
-(let (?e13 (ite (bvslt ?e12 ?e12) bv1[1] bv0[1]))
-(let (?e14 (ite (bvult ?e7 (sign_extend[4] ?e12)) bv1[1] bv0[1]))
-(let (?e15 (bvlshr (sign_extend[8] ?e4) v2))
-(let (?e16 (repeat[2] v0))
-(let (?e17 (rotate_right[4] ?e15))
-(let (?e18 (bvxor ?e14 ?e14))
-(let (?e19 (bvand v2 (sign_extend[7] ?e12)))
-(let (?e20 (bvnot v1))
-(flet ($e21 (= ?e15 ?e3))
-(flet ($e22 (= (sign_extend[6] ?e9) ?e8))
-(flet ($e23 (= ?e6 ?e4))
-(flet ($e24 (= ?e11 (zero_extend[2] ?e13)))
-(flet ($e25 (= v0 (zero_extend[2] ?e13)))
-(flet ($e26 (= (sign_extend[1] ?e4) ?e12))
-(flet ($e27 (= ?e15 ?e3))
-(flet ($e28 (= ?e3 ?e19))
-(flet ($e29 (= (zero_extend[8] ?e14) ?e15))
-(flet ($e30 (= v0 (sign_extend[2] ?e6)))
-(flet ($e31 (= ?e11 (sign_extend[2] ?e4)))
-(flet ($e32 (= ?e7 (zero_extend[5] ?e6)))
-(flet ($e33 (= ?e5 ?e5))
-(flet ($e34 (= (zero_extend[8] ?e6) v2))
-(flet ($e35 (= ?e20 (zero_extend[3] ?e3)))
-(flet ($e36 (= (zero_extend[8] ?e4) ?e15))
-(flet ($e37 (= ?e3 (sign_extend[8] ?e5)))
-(flet ($e38 (= (sign_extend[11] ?e9) v1))
-(flet ($e39 (= (zero_extend[1] ?e9) ?e12))
-(flet ($e40 (= (sign_extend[6] v0) ?e15))
-(flet ($e41 (= ?e7 (zero_extend[5] ?e14)))
-(flet ($e42 (= ?e6 ?e14))
-(flet ($e43 (= ?e16 (zero_extend[5] ?e4)))
-(flet ($e44 (= (zero_extend[8] ?e9) v2))
-(flet ($e45 (= v1 (zero_extend[11] ?e5)))
-(flet ($e46 (= ?e8 (zero_extend[6] ?e4)))
-(flet ($e47 (= (sign_extend[1] ?e13) ?e12))
-(flet ($e48 (= (zero_extend[11] ?e18) v1))
-(flet ($e49 (= (zero_extend[11] ?e5) v1))
-(flet ($e50 (= ?e15 (sign_extend[8] ?e4)))
-(flet ($e51 (= ?e13 ?e14))
-(flet ($e52 (= (zero_extend[2] ?e5) ?e11))
-(flet ($e53 (= (sign_extend[11] ?e9) v1))
-(flet ($e54 (= ?e8 (sign_extend[6] ?e5)))
-(flet ($e55 (= (sign_extend[7] ?e12) v2))
-(flet ($e56 (= ?e20 (sign_extend[3] ?e15)))
-(flet ($e57 (= ?e15 (sign_extend[6] ?e11)))
-(flet ($e58 (= ?e6 ?e4))
-(flet ($e59 (= (sign_extend[8] ?e10) v2))
-(flet ($e60 (= (zero_extend[8] ?e10) ?e19))
-(flet ($e61 (= ?e9 ?e6))
-(flet ($e62 (= ?e11 (sign_extend[2] ?e9)))
-(flet ($e63 (= v2 (zero_extend[8] ?e18)))
-(flet ($e64 (= (sign_extend[2] ?e10) ?e11))
-(flet ($e65 (= ?e5 ?e5))
-(flet ($e66 (= (zero_extend[3] ?e16) ?e17))
-(flet ($e67 (if_then_else $e34 $e37 $e22))
-(flet ($e68 (xor $e61 $e63))
-(flet ($e69 (iff $e55 $e53))
-(flet ($e70 (not $e51))
-(flet ($e71 (or $e70 $e56))
-(flet ($e72 (or $e23 $e54))
-(flet ($e73 (or $e43 $e39))
-(flet ($e74 (implies $e58 $e32))
-(flet ($e75 (and $e21 $e59))
-(flet ($e76 (implies $e33 $e38))
-(flet ($e77 (and $e41 $e57))
-(flet ($e78 (if_then_else $e77 $e74 $e64))
-(flet ($e79 (iff $e36 $e52))
-(flet ($e80 (or $e29 $e25))
-(flet ($e81 (iff $e68 $e62))
-(flet ($e82 (xor $e78 $e76))
-(flet ($e83 (xor $e66 $e69))
-(flet ($e84 (or $e45 $e27))
-(flet ($e85 (xor $e83 $e79))
-(flet ($e86 (if_then_else $e72 $e72 $e65))
-(flet ($e87 (iff $e28 $e75))
-(flet ($e88 (if_then_else $e26 $e73 $e47))
-(flet ($e89 (xor $e60 $e60))
-(flet ($e90 (xor $e49 $e42))
-(flet ($e91 (iff $e44 $e48))
-(flet ($e92 (and $e71 $e80))
-(flet ($e93 (not $e88))
-(flet ($e94 (iff $e35 $e35))
-(flet ($e95 (iff $e81 $e90))
-(flet ($e96 (xor $e89 $e85))
-(flet ($e97 (xor $e82 $e94))
-(flet ($e98 (or $e92 $e40))
-(flet ($e99 (implies $e93 $e24))
-(flet ($e100 (if_then_else $e46 $e31 $e50))
-(flet ($e101 (or $e86 $e97))
-(flet ($e102 (and $e101 $e67))
-(flet ($e103 (if_then_else $e87 $e96 $e30))
-(flet ($e104 (not $e100))
-(flet ($e105 (xor $e91 $e104))
-(flet ($e106 (if_then_else $e84 $e102 $e84))
-(flet ($e107 (implies $e106 $e98))
-(flet ($e108 (implies $e107 $e103))
-(flet ($e109 (or $e95 $e95))
-(flet ($e110 (implies $e108 $e109))
-(flet ($e111 (not $e99))
-(flet ($e112 (or $e110 $e105))
-(flet ($e113 (or $e112 $e112))
-(flet ($e114 (xor $e111 $e113))
-$e114
-)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-