(benchmark fuzzsmt
:logic QF_BV
:status unsat
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v3 BitVec[4]))
:formula
(let (?e4 bv12[4])
(let (?e5 bv14[4])
(let (?e6 bv5[4])
(let (?e7 bv6[4])
(let (?e8 bv13[4])
(let (?e9 (bvneg v0))
(let (?e10 (rotate_left[0] v0))
(let (?e11 (bvxnor v3 ?e6))
(let (?e12 (bvnot v0))
(let (?e13 (bvnand v0 ?e10))
(let (?e14 (ite (bvslt v0 ?e4) bv1[1] bv0[1]))
(let (?e15 (bvnand ?e6 ?e11))
(let (?e16 (bvadd ?e13 ?e11))
(let (?e17 (bvadd ?e12 ?e8))
(let (?e18 (bvcomp ?e10 ?e15))
(let (?e19 (ite (bvsgt ?e8 ?e5) bv1[1] bv0[1]))
(let (?e20 (ite (bvugt (sign_extend[3] ?e19) ?e15) bv1[1] bv0[1]))
(let (?e21 (bvxor v2 (sign_extend[3] ?e18)))
(let (?e22 (bvadd ?e13 (zero_extend[3] ?e18)))
(let (?e23 (ite (= ?e10 ?e13) bv1[1] bv0[1]))
(let (?e24 (ite (bvslt ?e9 (sign_extend[3] ?e23)) bv1[1] bv0[1]))
(let (?e25 (ite (bvsgt ?e8 (sign_extend[3] ?e24)) bv1[1] bv0[1]))
(let (?e26 (bvxnor ?e8 (zero_extend[3] ?e14)))
(let (?e27 (zero_extend[0] ?e25))
(let (?e28 (extract[0:0] ?e15))
(let (?e29 (ite (= (zero_extend[3] ?e19) ?e22) bv1[1] bv0[1]))
(let (?e30 (rotate_right[1] ?e9))
(let (?e31 (bvmul ?e10 v0))
(let (?e32 (bvmul (zero_extend[3] ?e20) ?e10))
(let (?e33 (bvshl ?e6 (sign_extend[3] ?e29)))
(let (?e34 (ite (bvuge ?e15 (zero_extend[3] ?e28)) bv1[1] bv0[1]))
(let (?e35 (bvmul (sign_extend[3] ?e18) ?e16))
(let (?e36 (rotate_left[0] ?e22))
(let (?e37 (bvshl v3 ?e15))
(let (?e38 (ite (bvsgt ?e30 ?e8) bv1[1] bv0[1]))
(let (?e39 (bvadd ?e30 (sign_extend[3] ?e27)))
(let (?e40 (ite (bvsle v1 ?e15) bv1[1] bv0[1]))
(let (?e41 (bvlshr ?e8 (zero_extend[3] ?e14)))
(let (?e42 (ite (bvsgt ?e32 ?e22) bv1[1] bv0[1]))
(let (?e43 (rotate_right[1] ?e31))
(let (?e44 (ite (bvsge (sign_extend[3] ?e19) ?e10) bv1[1] bv0[1]))
(let (?e45 (bvxor ?e12 ?e39))
(let (?e46 (ite (= (zero_extend[3] ?e19) ?e4) bv1[1] bv0[1]))
(let (?e47 (zero_extend[3] ?e18))
(let (?e48 (zero_extend[2] ?e20))
(let (?e49 (ite (bvslt ?e16 (zero_extend[3] ?e18)) bv1[1] bv0[1]))
(let (?e50 (bvnand ?e25 ?e29))
(let (?e51 (ite (= ?e15 ?e9) bv1[1] bv0[1]))
(let (?e52 (bvcomp ?e12 ?e6))
(let (?e53 (concat ?e51 ?e42))
(let (?e54 (bvnand ?e27 ?e29))
(let (?e55 (bvnor ?e26 ?e39))
(let (?e56 (bvand (sign_extend[3] ?e46) ?e41))
(let (?e57 (bvnor ?e4 ?e36))
(let (?e58 (repeat[2] ?e44))
(let (?e59 (ite (bvslt (sign_extend[3] ?e46) ?e17) bv1[1] bv0[1]))
(let (?e60 (bvxnor (sign_extend[3] ?e20) ?e21))
(let (?e61 (bvxnor v0 ?e35))
(let (?e62 (bvnor ?e6 ?e60))
(let (?e63 (ite (bvugt ?e29 ?e28) bv1[1] bv0[1]))
(let (?e64 (ite (bvule ?e23 ?e49) bv1[1] bv0[1]))
(let (?e65 (bvnot ?e23))
(let (?e66 (repeat[1] ?e5))
(let (?e67 (rotate_left[1] ?e17))
(let (?e68 (ite (bvsle ?e56 ?e61) bv1[1] bv0[1]))
(let (?e69 (sign_extend[0] ?e6))
(let (?e70 (ite (bvslt ?e31 (sign_extend[3] ?e44)) bv1[1] bv0[1]))
(let (?e71 (ite (= bv1[1] (extract[0:0] ?e17)) (zero_extend[3] ?e18) ?e41))
(let (?e72 (bvor (zero_extend[3] ?e28) ?e12))
(let (?e73 (bvashr ?e8 (sign_extend[3] ?e23)))
(let (?e74 (extract[0:0] ?e70))
(let (?e75 (bvnor ?e67 ?e62))
(let (?e76 (zero_extend[0] ?e61))
(let (?e77 (bvlshr ?e51 ?e54))
(let (?e78 (bvand ?e7 ?e8))
(flet ($e79 (bvule ?e19 ?e59))
(flet ($e80 (= ?e30 (zero_extend[3] ?e19)))
(flet ($e81 (bvult ?e28 ?e38))
(flet ($e82 (bvslt ?e7 ?e31))
(flet ($e83 (bvsgt ?e47 (sign_extend[3] ?e29)))
(flet ($e84 (bvslt ?e30 (sign_extend[3] ?e18)))
(flet ($e85 (= (sign_extend[3] ?e46) ?e47))
(flet ($e86 (distinct ?e61 ?e36))
(flet ($e87 (bvsge v3 (sign_extend[3] ?e52)))
(flet ($e88 (bvslt ?e56 ?e75))
(flet ($e89 (bvult ?e52 ?e14))
(flet ($e90 (bvslt ?e12 (sign_extend[3] ?e29)))
(flet ($e91 (bvslt ?e66 ?e76))
(flet ($e92 (bvult ?e37 ?e36))
(flet ($e93 (bvsgt ?e73 ?e69))
(flet ($e94 (bvslt ?e33 (zero_extend[3] ?e64)))
(flet ($e95 (distinct ?e75 (sign_extend[3] ?e54)))
(flet ($e96 (bvsge ?e30 ?e75))
(flet ($e97 (bvult (zero_extend[3] ?e25) ?e15))
(flet ($e98 (bvsle (zero_extend[3] ?e40) v1))
(flet ($e99 (bvsgt ?e32 ?e16))
(flet ($e100 (bvuge (sign_extend[1] ?e54) ?e58))
(flet ($e101 (bvuge ?e61 ?e41))
(flet ($e102 (bvsle ?e4 ?e10))
(flet ($e103 (bvsge ?e60 (zero_extend[1] ?e48)))
(flet ($e104 (bvugt ?e73 ?e17))
(flet ($e105 (bvugt ?e12 (sign_extend[3] ?e18)))
(flet ($e106 (bvslt ?e11 ?e11))
(flet ($e107 (bvugt (sign_extend[2] ?e58) v3))
(flet ($e108 (bvuge (sign_extend[1] ?e48) ?e66))
(flet ($e109 (distinct ?e30 ?e17))
(flet ($e110 (bvslt ?e33 ?e43))
(flet ($e111 (bvule ?e63 ?e25))
(flet ($e112 (= ?e35 ?e30))
(flet ($e113 (bvsgt ?e16 ?e33))
(flet ($e114 (= (zero_extend[3] ?e34) ?e26))
(flet ($e115 (distinct v0 (sign_extend[3] ?e28)))
(flet ($e116 (bvsge (zero_extend[3] ?e18) ?e6))
(flet ($e117 (= ?e15 ?e31))
(flet ($e118 (bvult (zero_extend[1] ?e40) ?e53))
(flet ($e119 (distinct (sign_extend[3] ?e28) ?e30))
(flet ($e120 (bvsge ?e16 v1))
(flet ($e121 (bvsge (sign_extend[3] ?e19) ?e78))
(flet ($e122 (bvule ?e59 ?e38))
(flet ($e123 (bvugt ?e73 v2))
(flet ($e124 (distinct ?e75 (sign_extend[3] ?e27)))
(flet ($e125 (bvslt (zero_extend[1] ?e59) ?e58))
(flet ($e126 (bvsge ?e12 ?e21))
(flet ($e127 (= ?e41 ?e12))
(flet ($e128 (bvugt ?e56 v1))
(flet ($e129 (bvsgt (zero_extend[3] ?e50) ?e45))
(flet ($e130 (= (sign_extend[2] ?e58) ?e57))
(flet ($e131 (bvugt ?e73 ?e10))
(flet ($e132 (bvult ?e4 ?e47))
(flet ($e133 (= (sign_extend[3] ?e68) ?e60))
(flet ($e134 (bvugt (sign_extend[3] ?e74) ?e33))
(flet ($e135 (bvult (sign_extend[3] ?e68) ?e47))
(flet ($e136 (bvslt ?e49 ?e63))
(flet ($e137 (bvugt ?e45 ?e13))
(flet ($e138 (bvugt ?e51 ?e19))
(flet ($e139 (bvslt ?e30 (sign_extend[3] ?e68)))
(flet ($e140 (distinct (zero_extend[3] ?e52) v1))
(flet ($e141 (= ?e17 ?e60))
(flet ($e142 (bvuge ?e40 ?e77))
(flet ($e143 (bvsge (sign_extend[3] ?e18) ?e5))
(flet ($e144 (bvult ?e35 (sign_extend[3] ?e27)))
(flet ($e145 (bvsgt ?e60 (zero_extend[3] ?e14)))
(flet ($e146 (bvsle ?e26 (zero_extend[3] ?e27)))
(flet ($e147 (bvule ?e72 ?e57))
(flet ($e148 (= ?e41 (sign_extend[3] ?e59)))
(flet ($e149 (bvuge (sign_extend[3] ?e52) ?e45))
(flet ($e150 (bvule (sign_extend[3] ?e70) v2))
(flet ($e151 (bvslt v1 (sign_extend[3] ?e49)))
(flet ($e152 (distinct ?e22 (sign_extend[1] ?e48)))
(flet ($e153 (distinct v1 ?e15))
(flet ($e154 (bvuge ?e5 ?e62))
(flet ($e155 (= ?e12 v3))
(flet ($e156 (bvsge (zero_extend[3] ?e68) ?e62))
(flet ($e157 (bvuge ?e76 (zero_extend[3] ?e65)))
(flet ($e158 (= ?e26 ?e55))
(flet ($e159 (bvsgt (zero_extend[3] ?e54) ?e72))
(flet ($e160 (bvsle (sign_extend[3] ?e29) ?e41))
(flet ($e161 (= (zero_extend[3] ?e18) v1))
(flet ($e162 (bvsle ?e8 (sign_extend[3] ?e46)))
(flet ($e163 (bvule ?e21 (zero_extend[3] ?e65)))
(flet ($e164 (bvuge ?e36 (zero_extend[3] ?e64)))
(flet ($e165 (= (zero_extend[3] ?e18) ?e43))
(flet ($e166 (bvugt v0 (sign_extend[3] ?e70)))
(flet ($e167 (bvslt (sign_extend[3] ?e24) ?e60))
(flet ($e168 (bvsgt ?e10 (sign_extend[2] ?e53)))
(flet ($e169 (bvugt ?e70 ?e70))
(flet ($e170 (bvuge (sign_extend[3] ?e34) ?e43))
(flet ($e171 (bvult ?e65 ?e19))
(flet ($e172 (bvult ?e71 ?e17))
(flet ($e173 (= ?e7 (zero_extend[3] ?e64)))
(flet ($e174 (bvslt v0 ?e78))
(flet ($e175 (bvsge ?e60 ?e78))
(flet ($e176 (bvuge v2 ?e10))
(flet ($e177 (bvsge ?e34 ?e40))
(flet ($e178 (bvuge (sign_extend[3] ?e49) ?e17))
(flet ($e179 (bvuge ?e71 (zero_extend[3] ?e14)))
(flet ($e180 (bvult ?e66 (sign_extend[3] ?e25)))
(flet ($e181 (bvsge (sign_extend[3] ?e23) v2))
(flet ($e182 (bvsge ?e64 ?e65))
(flet ($e183 (bvugt ?e72 ?e8))
(flet ($e184 (bvule ?e70 ?e34))
(flet ($e185 (distinct ?e25 ?e49))
(flet ($e186 (bvsgt ?e41 (sign_extend[3] ?e40)))
(flet ($e187 (bvslt ?e26 (sign_extend[3] ?e42)))
(flet ($e188 (bvsgt ?e9 (sign_extend[3] ?e23)))
(flet ($e189 (distinct ?e56 ?e21))
(flet ($e190 (bvugt ?e35 v2))
(flet ($e191 (bvsle ?e61 ?e33))
(flet ($e192 (bvsge (sign_extend[3] ?e46) ?e69))
(flet ($e193 (= ?e27 ?e18))
(flet ($e194 (bvsgt ?e75 (zero_extend[3] ?e52)))
(flet ($e195 (bvsgt ?e36 (sign_extend[3] ?e18)))
(flet ($e196 (bvsgt (zero_extend[3] ?e20) ?e15))
(flet ($e197 (bvsge ?e78 ?e36))
(flet ($e198 (= (sign_extend[3] ?e51) ?e4))
(flet ($e199 (bvsge ?e47 ?e37))
(flet ($e200 (bvsgt ?e5 (sign_extend[3] ?e51)))
(flet ($e201 (bvsgt ?e13 ?e75))
(flet ($e202 (bvsle ?e15 ?e55))
(flet ($e203 (bvsgt ?e47 ?e33))
(flet ($e204 (bvsle (sign_extend[3] ?e28) v1))
(flet ($e205 (bvsle (sign_extend[3] ?e77) ?e13))
(flet ($e206 (bvsgt ?e48 (zero_extend[2] ?e46)))
(flet ($e207 (bvsgt (zero_extend[3] ?e52) ?e56))
(flet ($e208 (bvule (zero_extend[3] ?e46) ?e21))
(flet ($e209 (bvuge ?e9 (zero_extend[3] ?e40)))
(flet ($e210 (bvuge (sign_extend[3] ?e46) ?e26))
(flet ($e211 (bvule (zero_extend[3] ?e40) ?e55))
(flet ($e212 (distinct ?e12 v2))
(flet ($e213 (distinct v2 ?e4))
(flet ($e214 (bvslt ?e63 ?e65))
(flet ($e215 (bvsge ?e28 ?e77))
(flet ($e216 (bvsle (zero_extend[3] ?e70) ?e11))
(flet ($e217 (bvult (sign_extend[3] ?e49) v0))
(flet ($e218 (bvslt ?e76 ?e72))
(flet ($e219 (bvuge ?e28 ?e14))
(flet ($e220 (bvsgt ?e7 ?e7))
(flet ($e221 (bvuge ?e53 (zero_extend[1] ?e28)))
(flet ($e222 (bvslt (zero_extend[3] ?e27) ?e33))
(flet ($e223 (bvuge (sign_extend[3] ?e38) ?e57))
(flet ($e224 (bvugt ?e44 ?e14))
(flet ($e225 (bvugt ?e36 (sign_extend[3] ?e44)))
(flet ($e226 (bvugt ?e41 ?e41))
(flet ($e227 (bvsge v2 ?e35))
(flet ($e228 (distinct ?e9 v1))
(flet ($e229 (bvuge ?e25 ?e42))
(flet ($e230 (bvsgt (sign_extend[3] ?e40) ?e66))
(flet ($e231 (bvule ?e24 ?e14))
(flet ($e232 (bvsge ?e62 ?e37))
(flet ($e233 (bvsge ?e47 ?e16))
(flet ($e234 (bvugt ?e32 (sign_extend[3] ?e51)))
(flet ($e235 (bvule ?e6 ?e15))
(flet ($e236 (bvuge ?e36 ?e57))
(flet ($e237 (bvult ?e9 ?e16))
(flet ($e238 (bvule ?e56 (zero_extend[3] ?e51)))
(flet ($e239 (bvsgt ?e15 (zero_extend[3] ?e23)))
(flet ($e240 (bvugt (zero_extend[3] ?e18) ?e21))
(flet ($e241 (bvsge v3 (zero_extend[3] ?e40)))
(flet ($e242 (bvult ?e36 (zero_extend[3] ?e59)))
(flet ($e243 (bvugt ?e75 (zero_extend[1] ?e48)))
(flet ($e244 (bvult ?e21 ?e33))
(flet ($e245 (= ?e32 v2))
(flet ($e246 (bvsgt ?e21 ?e69))
(flet ($e247 (bvsle ?e7 ?e37))
(flet ($e248 (distinct (sign_extend[3] ?e64) ?e12))
(flet ($e249 (distinct v0 (sign_extend[3] ?e27)))
(flet ($e250 (distinct (sign_extend[3] ?e42) ?e56))
(flet ($e251 (bvult ?e56 ?e22))
(flet ($e252 (bvslt ?e7 ?e6))
(flet ($e253 (bvsle ?e31 ?e16))
(flet ($e254 (bvslt v1 (zero_extend[3] ?e18)))
(flet ($e255 (bvuge ?e15 ?e30))
(flet ($e256 (distinct ?e45 ?e11))
(flet ($e257 (distinct ?e7 ?e66))
(flet ($e258 (bvule ?e56 (zero_extend[1] ?e48)))
(flet ($e259 (bvugt ?e26 ?e55))
(flet ($e260 (bvsle ?e39 (zero_extend[3] ?e14)))
(flet ($e261 (bvsgt ?e75 ?e67))
(flet ($e262 
(and
 (or (not $e246) $e254 $e237)
 (or (not $e151) (not $e150) $e92)
 (or (not $e177) (not $e178) (not $e205))
 (or $e82 (not $e127) $e187)
 (or (not $e169) $e88 (not $e90))
 (or (not $e98) $e130 (not $e87))
 (or (not $e235) $e207 $e129)
 (or (not $e163) (not $e207) $e109)
 (or (not $e236) (not $e124) $e123)
 (or (not $e194) $e261 $e178)
 (or $e172 $e159 (not $e261))
 (or $e154 $e100 $e123)
 (or (not $e195) $e213 $e194)
 (or (not $e184) (not $e202) (not $e137))
 (or (not $e81) (not $e248) $e92)
 (or $e119 $e189 $e223)
 (or $e199 (not $e160) (not $e208))
 (or (not $e85) (not $e82) (not $e170))
 (or (not $e153) (not $e172) $e119)
 (or (not $e182) $e151 (not $e257))
 (or (not $e243) $e224 (not $e192))
 (or (not $e79) (not $e152) (not $e100))
 (or (not $e178) $e158 $e195)
 (or (not $e148) (not $e146) $e166)
 (or $e235 (not $e152) (not $e255))
 (or (not $e177) (not $e237) (not $e138))
 (or $e210 (not $e191) (not $e95))
 (or $e138 $e260 (not $e232))
 (or $e180 (not $e112) (not $e96))
 (or (not $e223) (not $e215) $e137)
 (or (not $e175) (not $e192) (not $e170))
 (or (not $e175) (not $e256) (not $e138))
 (or $e91 $e143 $e147)
 (or $e253 $e206 $e217)
 (or $e249 (not $e205) $e252)
 (or $e153 $e212 $e151)
 (or $e175 $e84 (not $e105))
 (or (not $e210) $e185 $e236)
 (or (not $e83) $e248 $e165)
 (or $e202 (not $e106) $e145)
 (or (not $e129) (not $e153) (not $e235))
 (or $e253 (not $e122) (not $e174))
 (or $e191 (not $e209) (not $e235))
 (or $e256 $e216 (not $e142))
 (or $e237 (not $e132) $e81)
 (or $e121 (not $e250) $e162)
 (or $e175 (not $e133) (not $e82))
 (or $e217 (not $e90) (not $e220))
 (or $e210 $e188 (not $e124))
 (or (not $e153) (not $e110) $e229)
 (or (not $e224) $e177 $e83)
 (or (not $e233) $e170 (not $e233))
 (or (not $e152) $e241 $e178)
 (or $e192 (not $e209) $e177)
 (or $e191 $e143 (not $e117))
 (or (not $e133) $e91 (not $e120))
 (or (not $e227) (not $e217) $e197)
 (or (not $e99) (not $e223) (not $e261))
 (or $e139 $e85 $e128)
 (or $e219 (not $e156) (not $e208))
 (or (not $e112) (not $e219) $e235)
 (or $e104 (not $e98) (not $e190))
 (or $e247 (not $e129) (not $e254))
 (or $e110 $e186 $e225)
 (or $e215 $e170 $e135)
 (or $e92 (not $e256) (not $e143))
 (or $e160 (not $e89) $e173)
 (or $e238 (not $e188) (not $e144))
 (or $e164 (not $e247) (not $e87))
 (or $e83 $e251 (not $e169))
 (or (not $e149) (not $e166) $e97)
 (or (not $e205) (not $e166) (not $e218))
 (or $e163 (not $e137) $e190)
 (or (not $e151) (not $e207) (not $e144))
 (or (not $e110) $e84 (not $e82))
 (or $e211 (not $e105) (not $e117))
 (or $e233 $e218 (not $e188))
 (or $e165 $e197 $e235)
 (or $e107 (not $e222) (not $e203))
 (or $e157 (not $e215) $e245)
 (or $e140 $e151 (not $e255))
 (or $e126 $e192 (not $e225))
 (or (not $e257) (not $e143) $e213)
 (or $e100 (not $e98) $e103)
 (or (not $e173) $e132 $e113)
 (or $e250 (not $e250) $e122)
 (or $e201 $e119 $e230)
 (or $e128 (not $e184) (not $e228))
 (or $e211 $e120 (not $e124))
 (or (not $e80) $e91 $e139)
 (or $e205 (not $e220) $e91)
))
$e262
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))