(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
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))