1 files changed, 0 insertions, 304 deletions
diff --git a/test/regress/regress0/bv/fuzz35.smt b/test/regress/regress0/bv/fuzz35.smt
deleted file mode 100644
index 73ae721b2..000000000
--- a/test/regress/regress0/bv/fuzz35.smt
+++ /dev/null
@@ -1,304 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_BV
-:status unsat
-:extrafuns ((v0 BitVec[4]))
-:extrafuns ((v1 BitVec[4]))
-:extrafuns ((v2 BitVec[4]))
-:extrafuns ((v3 BitVec[4]))
-:extrafuns ((v4 BitVec[4]))
-:formula
-(let (?e5 bv4[4])
-(let (?e6 bv12[4])
-(let (?e7 bv4[4])
-(let (?e8 (bvlshr ?e5 v0))
-(let (?e9 (ite (= bv1[1] (extract[1:1] ?e5)) v2 v1))
-(let (?e10 (bvsub ?e7 ?e6))
-(let (?e11 (zero_extend[0] ?e7))
-(let (?e12 (sign_extend[0] ?e9))
-(let (?e13 (bvnot ?e7))
-(let (?e14 (bvlshr ?e7 v3))
-(let (?e15 (extract[1:0] v0))
-(let (?e16 (bvneg ?e10))
-(let (?e17 (ite (= ?e9 v2) bv1[1] bv0[1]))
-(let (?e18 (bvmul ?e10 v0))
-(let (?e19 (bvadd ?e8 ?e14))
-(let (?e20 (zero_extend[0] ?e18))
-(let (?e21 (bvmul ?e8 ?e18))
-(let (?e22 (bvsub ?e11 ?e14))
-(let (?e23 (ite (bvugt v1 ?e5) bv1[1] bv0[1]))
-(let (?e24 (bvashr ?e14 ?e18))
-(let (?e25 (bvadd ?e21 ?e9))
-(let (?e26 (bvadd ?e20 ?e20))
-(let (?e27 (ite (bvslt (zero_extend[3] ?e23) v3) bv1[1] bv0[1]))
-(let (?e28 (ite (bvugt ?e9 ?e12) bv1[1] bv0[1]))
-(let (?e29 (bvnot ?e26))
-(let (?e30 (ite (bvult ?e21 ?e11) bv1[1] bv0[1]))
-(let (?e31 (bvsub v1 ?e20))
-(let (?e32 (ite (bvslt ?e19 (zero_extend[3] ?e28)) bv1[1] bv0[1]))
-(let (?e33 (rotate_right[0] ?e15))
-(let (?e34 (bvnot ?e14))
-(let (?e35 (zero_extend[0] ?e24))
-(let (?e36 (sign_extend[0] ?e22))
-(let (?e37 (ite (bvult ?e25 ?e10) bv1[1] bv0[1]))
-(let (?e38 (bvashr ?e27 ?e23))
-(let (?e39 (bvcomp v0 ?e31))
-(let (?e40 (bvand v0 ?e31))
-(let (?e41 (zero_extend[0] ?e21))
-(let (?e42 (ite (= bv1[1] (extract[0:0] ?e14)) ?e40 (sign_extend[3] ?e23)))
-(let (?e43 (sign_extend[0] ?e32))
-(let (?e44 (sign_extend[0] ?e19))
-(let (?e45 (ite (= bv1[1] (extract[2:2] ?e40)) (sign_extend[3] ?e27) ?e24))
-(let (?e46 (bvnot ?e21))
-(let (?e47 (rotate_right[3] v3))
-(let (?e48 (bvxnor (zero_extend[2] ?e15) ?e45))
-(let (?e49 (bvand ?e40 ?e46))
-(let (?e50 (ite (bvsle ?e20 ?e31) bv1[1] bv0[1]))
-(let (?e51 (bvneg ?e22))
-(let (?e52 (bvor ?e41 ?e22))
-(let (?e53 (ite (bvslt v1 ?e13) bv1[1] bv0[1]))
-(let (?e54 (bvshl ?e11 (sign_extend[3] ?e38)))
-(let (?e55 (ite (bvsge (zero_extend[3] ?e17) ?e40) bv1[1] bv0[1]))
-(let (?e56 (ite (distinct ?e52 (zero_extend[3] ?e17)) bv1[1] bv0[1]))
-(let (?e57 (bvneg ?e17))
-(let (?e58 (extract[3:0] ?e47))
-(let (?e59 (ite (bvugt ?e30 ?e17) bv1[1] bv0[1]))
-(let (?e60 (zero_extend[0] ?e48))
-(let (?e61 (bvshl (sign_extend[3] ?e59) v4))
-(flet ($e62 (bvsgt ?e60 (zero_extend[3] ?e57)))
-(flet ($e63 (bvule ?e15 (zero_extend[1] ?e38)))
-(flet ($e64 (distinct ?e16 (sign_extend[3] ?e30)))
-(flet ($e65 (= ?e25 ?e14))
-(flet ($e66 (bvsgt (sign_extend[3] ?e43) ?e10))
-(flet ($e67 (bvule (sign_extend[3] ?e39) ?e41))
-(flet ($e68 (bvult ?e25 ?e36))
-(flet ($e69 (bvugt ?e36 ?e24))
-(flet ($e70 (bvslt (zero_extend[3] ?e50) ?e12))
-(flet ($e71 (bvsle ?e25 (zero_extend[3] ?e32)))
-(flet ($e72 (bvsgt ?e37 ?e57))
-(flet ($e73 (bvuge ?e48 ?e47))
-(flet ($e74 (bvsle v2 ?e41))
-(flet ($e75 (bvule ?e48 (zero_extend[3] ?e53)))
-(flet ($e76 (bvsge (zero_extend[1] ?e28) ?e33))
-(flet ($e77 (distinct ?e33 (sign_extend[1] ?e55)))
-(flet ($e78 (bvule ?e27 ?e53))
-(flet ($e79 (= ?e55 ?e55))
-(flet ($e80 (bvule ?e55 ?e17))
-(flet ($e81 (bvuge ?e47 (sign_extend[3] ?e39)))
-(flet ($e82 (= ?e26 ?e22))
-(flet ($e83 (bvslt (sign_extend[2] ?e15) ?e35))
-(flet ($e84 (bvugt ?e23 ?e53))
-(flet ($e85 (bvslt ?e22 (zero_extend[3] ?e56)))
-(flet ($e86 (bvuge ?e10 (sign_extend[3] ?e38)))
-(flet ($e87 (bvsge ?e24 (zero_extend[3] ?e57)))
-(flet ($e88 (bvsgt ?e29 ?e21))
-(flet ($e89 (= ?e8 (sign_extend[3] ?e37)))
-(flet ($e90 (bvslt ?e41 ?e24))
-(flet ($e91 (bvsgt v3 (sign_extend[3] ?e43)))
-(flet ($e92 (= ?e57 ?e55))
-(flet ($e93 (bvsgt ?e16 (sign_extend[3] ?e28)))
-(flet ($e94 (bvsge (sign_extend[3] ?e37) v0))
-(flet ($e95 (bvsge ?e13 ?e44))
-(flet ($e96 (bvsle ?e18 ?e18))
-(flet ($e97 (bvuge ?e17 ?e38))
-(flet ($e98 (bvugt ?e51 ?e42))
-(flet ($e99 (= ?e47 ?e49))
-(flet ($e100 (bvule ?e43 ?e39))
-(flet ($e101 (bvsle ?e47 ?e45))
-(flet ($e102 (bvuge (zero_extend[3] ?e50) v3))
-(flet ($e103 (distinct ?e5 ?e34))
-(flet ($e104 (bvugt (zero_extend[3] ?e38) ?e29))
-(flet ($e105 (bvuge (sign_extend[3] ?e38) ?e58))
-(flet ($e106 (bvsge ?e28 ?e56))
-(flet ($e107 (distinct ?e51 ?e10))
-(flet ($e108 (bvsge ?e21 ?e10))
-(flet ($e109 (bvsle (zero_extend[3] ?e32) ?e5))
-(flet ($e110 (bvsle ?e7 (sign_extend[3] ?e38)))
-(flet ($e111 (bvugt ?e8 v3))
-(flet ($e112 (= ?e21 ?e49))
-(flet ($e113 (bvugt ?e34 (sign_extend[3] ?e27)))
-(flet ($e114 (bvugt (sign_extend[3] ?e50) v3))
-(flet ($e115 (= ?e25 ?e6))
-(flet ($e116 (distinct ?e13 (sign_extend[3] ?e27)))
-(flet ($e117 (bvugt ?e10 ?e7))
-(flet ($e118 (= ?e8 ?e58))
-(flet ($e119 (bvsgt ?e45 ?e42))
-(flet ($e120 (distinct ?e38 ?e53))
-(flet ($e121 (bvule (zero_extend[3] ?e50) ?e35))
-(flet ($e122 (distinct ?e51 ?e25))
-(flet ($e123 (bvslt v4 ?e44))
-(flet ($e124 (= ?e14 v0))
-(flet ($e125 (bvsge (zero_extend[1] ?e39) ?e33))
-(flet ($e126 (bvslt v0 (zero_extend[3] ?e57)))
-(flet ($e127 (bvsle ?e6 ?e36))
-(flet ($e128 (bvugt ?e13 (zero_extend[3] ?e28)))
-(flet ($e129 (bvsle ?e40 v1))
-(flet ($e130 (bvuge (sign_extend[3] ?e23) ?e44))
-(flet ($e131 (bvule (sign_extend[3] ?e56) ?e41))
-(flet ($e132 (bvule ?e20 ?e13))
-(flet ($e133 (bvult ?e6 (sign_extend[2] ?e15)))
-(flet ($e134 (bvugt ?e51 (zero_extend[3] ?e28)))
-(flet ($e135 (bvslt ?e10 (zero_extend[3] ?e57)))
-(flet ($e136 (= (zero_extend[3] ?e32) ?e14))
-(flet ($e137 (bvsge ?e29 ?e47))
-(flet ($e138 (= v3 ?e54))
-(flet ($e139 (= ?e60 ?e16))
-(flet ($e140 (bvsgt ?e24 ?e52))
-(flet ($e141 (bvuge v0 ?e34))
-(flet ($e142 (distinct v1 ?e34))
-(flet ($e143 (bvugt ?e61 v2))
-(flet ($e144 (bvsgt ?e33 (sign_extend[1] ?e27)))
-(flet ($e145 (bvsgt ?e55 ?e27))
-(flet ($e146 (bvsgt (zero_extend[3] ?e32) ?e61))
-(flet ($e147 (bvsgt ?e44 (zero_extend[3] ?e43)))
-(flet ($e148 (= ?e42 ?e45))
-(flet ($e149 (bvult ?e51 (zero_extend[3] ?e37)))
-(flet ($e150 (bvugt ?e31 ?e54))
-(flet ($e151 (bvsle ?e41 ?e22))
-(flet ($e152 (bvsge ?e20 ?e44))
-(flet ($e153 (bvsge (sign_extend[3] ?e50) ?e24))
-(flet ($e154 (distinct ?e45 ?e20))
-(flet ($e155 (= ?e29 (zero_extend[3] ?e30)))
-(flet ($e156 (bvslt ?e10 ?e44))
-(flet ($e157 (distinct ?e56 ?e30))
-(flet ($e158 (bvsle ?e17 ?e28))
-(flet ($e159 (bvuge ?e60 ?e44))
-(flet ($e160 (bvule ?e42 ?e24))
-(flet ($e161 (distinct ?e25 (sign_extend[3] ?e55)))
-(flet ($e162 (bvslt (sign_extend[3] ?e37) ?e21))
-(flet ($e163 (distinct ?e5 (sign_extend[3] ?e27)))
-(flet ($e164 (bvule ?e25 v1))
-(flet ($e165 (= v0 ?e60))
-(flet ($e166 (bvuge (sign_extend[3] ?e50) ?e26))
-(flet ($e167 (bvslt ?e58 ?e48))
-(flet ($e168 (bvsgt (sign_extend[3] ?e23) ?e42))
-(flet ($e169 (= ?e46 ?e34))
-(flet ($e170 (bvsgt ?e7 ?e20))
-(flet ($e171 (bvule ?e31 ?e12))
-(flet ($e172 (distinct ?e60 ?e18))
-(flet ($e173 (bvslt (sign_extend[3] ?e27) ?e40))
-(flet ($e174 (bvsge ?e42 ?e49))
-(flet ($e175 (bvugt ?e26 ?e11))
-(flet ($e176 (bvsgt ?e20 ?e35))
-(flet ($e177 (bvult ?e19 ?e19))
-(flet ($e178 (= ?e25 ?e10))
-(flet ($e179 (bvule (sign_extend[3] ?e23) ?e45))
-(flet ($e180 (bvslt v2 v3))
-(flet ($e181 (bvsgt ?e42 ?e42))
-(flet ($e182 (bvugt ?e58 ?e54))
-(flet ($e183 (bvsle ?e61 (zero_extend[3] ?e37)))
-(flet ($e184 (bvslt ?e60 (zero_extend[3] ?e57)))
-(flet ($e185 (distinct ?e21 (zero_extend[3] ?e27)))
-(flet ($e186 (bvule ?e58 v0))
-(flet ($e187 (= (sign_extend[3] ?e43) ?e13))
-(flet ($e188 (bvsge ?e52 (zero_extend[3] ?e50)))
-(flet ($e189 (bvsle ?e10 ?e51))
-(flet ($e190 (= ?e52 ?e29))
-(flet ($e191 (= ?e49 ?e25))
-(flet ($e192 (bvslt ?e60 ?e46))
-(flet ($e193 (bvugt ?e12 (zero_extend[2] ?e33)))
-(flet ($e194 (bvult ?e37 ?e28))
-(flet ($e195 (bvslt ?e20 (sign_extend[3] ?e30)))
-(flet ($e196 (bvult ?e8 ?e7))
-(flet ($e197 (bvsge ?e53 ?e37))
-(flet ($e198 (bvule ?e56 ?e50))
-(flet ($e199 (bvuge ?e11 ?e12))
-(flet ($e200 (bvsgt ?e24 ?e51))
-(flet ($e201 (bvsle (zero_extend[3] ?e59) ?e40))
-(flet ($e202 (bvule ?e21 ?e47))
-(flet ($e203 (bvsge ?e60 ?e11))
-(flet ($e204 (bvuge (zero_extend[3] ?e38) ?e29))
-(flet ($e205 (distinct ?e58 (sign_extend[3] ?e38)))
-(flet ($e206 (bvuge ?e11 (zero_extend[2] ?e33)))
-(flet ($e207 (bvult ?e42 ?e11))
-(flet ($e208 (distinct ?e10 ?e26))
-(flet ($e209 (bvult ?e5 ?e54))
-(flet ($e210 (bvsgt ?e21 v2))
-(flet ($e211 (bvsgt ?e49 ?e34))
-(flet ($e212 (bvuge ?e29 (zero_extend[3] ?e23)))
-(flet ($e213 (bvult ?e45 ?e35))
-(flet ($e214 (bvult ?e45 (sign_extend[3] ?e50)))
-(flet ($e215 (bvsle ?e19 ?e18))
-(flet ($e216 (= ?e9 ?e52))
-(flet ($e217 
-(and
- (or (not $e88) $e135 $e139)
- (or $e160 (not $e134) $e82)
- (or (not $e215) $e85 (not $e71))
- (or $e121 (not $e131) $e147)
- (or $e101 (not $e188) (not $e174))
- (or $e158 $e68 (not $e167))
- (or $e90 $e63 $e138)
- (or $e169 $e131 $e121)
- (or $e185 (not $e109) (not $e169))
- (or (not $e204) (not $e197) (not $e75))
- (or (not $e209) (not $e165) (not $e94))
- (or (not $e182) $e189 $e142)
- (or $e160 (not $e202) (not $e172))
- (or $e164 $e187 $e148)
- (or $e155 (not $e166) $e118)
- (or (not $e102) (not $e113) $e109)
- (or (not $e160) (not $e196) (not $e213))
- (or $e116 $e128 (not $e80))
- (or (not $e111) (not $e163) (not $e159))
- (or (not $e80) $e118 $e197)
- (or (not $e149) (not $e121) $e72)
- (or $e64 (not $e173) $e126)
- (or (not $e140) (not $e189) $e95)
- (or $e98 $e78 (not $e207))
- (or (not $e115) $e117 $e123)
- (or (not $e112) $e204 $e193)
- (or (not $e158) $e190 (not $e103))
- (or $e63 $e178 $e213)
- (or $e134 (not $e215) $e101)
- (or $e132 $e116 $e72)
- (or (not $e63) (not $e174) $e161)
- (or (not $e90) (not $e120) (not $e145))
- (or (not $e147) (not $e201) (not $e195))
- (or (not $e157) (not $e90) $e187)
- (or $e205 (not $e164) $e104)
- (or $e100 $e178 $e96)
- (or (not $e62) (not $e134) $e152)
- (or (not $e87) (not $e146) $e150)
- (or $e80 (not $e183) $e147)
- (or (not $e215) (not $e110) $e193)
- (or $e182 (not $e152) (not $e164))
- (or (not $e93) (not $e67) (not $e82))
- (or (not $e95) (not $e172) $e115)
- (or (not $e216) (not $e120) (not $e92))
- (or (not $e82) (not $e80) $e164)
- (or $e159 (not $e208) (not $e194))
- (or $e159 (not $e134) (not $e185))
- (or (not $e115) (not $e119) (not $e209))
- (or $e200 $e126 (not $e127))
- (or $e82 $e71 $e157)
- (or (not $e75) (not $e163) (not $e117))
- (or $e134 $e117 $e197)
- (or $e64 $e80 (not $e171))
- (or (not $e197) (not $e108) (not $e156))
- (or $e124 (not $e171) (not $e183))
- (or (not $e159) $e110 (not $e215))
- (or $e195 $e203 $e79)
- (or (not $e147) $e107 $e163)
- (or $e67 $e170 (not $e215))
- (or (not $e94) (not $e127) (not $e124))
- (or (not $e125) (not $e192) $e87)
- (or $e139 (not $e86) $e88)
- (or (not $e164) (not $e76) (not $e116))
- (or $e120 $e116 $e180)
- (or (not $e165) (not $e175) $e76)
- (or (not $e117) (not $e187) (not $e159))
- (or $e122 (not $e69) (not $e127))
- (or $e142 $e123 $e103)
- (or (not $e178) (not $e155) $e73)
- (or $e139 (not $e202) $e170)
- (or $e103 $e205 (not $e136))
- (or (not $e86) $e115 $e87)
- (or (not $e205) (not $e173) $e65)
- (or (not $e67) $e69 (not $e93))
- (or (not $e98) $e159 $e121)
- (or (not $e136) $e132 $e90)
- (or (not $e105) (not $e103) $e212)
-))
-$e217
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-