(benchmark fuzzsmt
:logic QF_BV
:status unknown
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v3 BitVec[4]))
:extrafuns ((v4 BitVec[4]))
:formula
(let (?e5 bv15[4])
(let (?e6 bv11[4])
(let (?e7 bv13[4])
(let (?e8 bv11[4])
(let (?e9 (bvshl v3 v3))
(let (?e10 (bvmul ?e5 ?e5))
(let (?e11 (ite (bvuge ?e9 v0) bv1[1] bv0[1]))
(let (?e12 (bvnor v2 v2))
(let (?e13 (ite (= bv1[1] (extract[2:2] v4)) v1 v4))
(let (?e14 (bvashr ?e12 v0))
(let (?e15 (bvnor v2 v0))
(let (?e16 (bvnor v1 ?e10))
(let (?e17 (ite (= (sign_extend[3] ?e11) v2) bv1[1] bv0[1]))
(let (?e18 (ite (bvugt ?e7 ?e5) bv1[1] bv0[1]))
(let (?e19 (bvxnor ?e7 v4))
(let (?e20 (ite (bvule ?e9 v4) bv1[1] bv0[1]))
(let (?e21 (bvashr ?e6 (sign_extend[3] ?e18)))
(let (?e22 (bvxnor ?e7 ?e9))
(let (?e23 (bvadd ?e16 v0))
(let (?e24 (bvmul v0 ?e16))
(let (?e25 (ite (bvsge v2 ?e24) bv1[1] bv0[1]))
(let (?e26 (ite (bvslt ?e23 ?e15) bv1[1] bv0[1]))
(let (?e27 (bvnot ?e15))
(let (?e28 (ite (= bv1[1] (extract[0:0] v4)) ?e16 (sign_extend[3] ?e17)))
(let (?e29 (ite (= (sign_extend[3] ?e25) ?e12) bv1[1] bv0[1]))
(let (?e30 (bvadd ?e7 ?e23))
(let (?e31 (ite (bvuge (sign_extend[3] ?e26) ?e5) bv1[1] bv0[1]))
(let (?e32 (bvlshr v3 ?e27))
(let (?e33 (bvnand ?e10 ?e19))
(let (?e34 (sign_extend[1] ?e25))
(let (?e35 (ite (= v2 v0) bv1[1] bv0[1]))
(let (?e36 (zero_extend[0] ?e14))
(let (?e37 (repeat[1] ?e28))
(let (?e38 (ite (bvugt ?e17 ?e29) bv1[1] bv0[1]))
(let (?e39 (ite (bvuge v3 ?e24) bv1[1] bv0[1]))
(let (?e40 (ite (= ?e31 ?e17) bv1[1] bv0[1]))
(let (?e41 (ite (distinct ?e10 (sign_extend[3] ?e39)) bv1[1] bv0[1]))
(let (?e42 (zero_extend[0] ?e28))
(let (?e43 (sign_extend[0] ?e36))
(let (?e44 (ite (bvule ?e34 (sign_extend[1] ?e11)) bv1[1] bv0[1]))
(let (?e45 (bvxnor ?e22 ?e28))
(let (?e46 (bvashr (sign_extend[3] ?e38) ?e14))
(let (?e47 (rotate_left[0] ?e17))
(let (?e48 (ite (bvsle ?e46 ?e27) bv1[1] bv0[1]))
(let (?e49 (bvadd ?e15 (zero_extend[3] ?e25)))
(let (?e50 (bvmul ?e21 ?e24))
(let (?e51 (bvadd (sign_extend[3] ?e26) ?e50))
(let (?e52 (bvnor (sign_extend[3] ?e20) ?e43))
(let (?e53 (bvmul v0 v3))
(let (?e54 (bvnor v0 (sign_extend[3] ?e39)))
(let (?e55 (bvor ?e46 ?e5))
(let (?e56 (zero_extend[0] ?e50))
(let (?e57 (repeat[1] ?e15))
(let (?e58 (repeat[1] ?e5))
(let (?e59 (bvxor ?e51 v3))
(let (?e60 (bvcomp ?e58 ?e19))
(let (?e61 (ite (bvugt ?e28 ?e56) bv1[1] bv0[1]))
(let (?e62 (bvxnor ?e55 ?e53))
(let (?e63 (ite (bvsle ?e46 ?e30) bv1[1] bv0[1]))
(let (?e64 (ite (bvsle ?e51 ?e28) bv1[1] bv0[1]))
(let (?e65 (bvshl ?e15 ?e59))
(let (?e66 (ite (bvult ?e10 ?e42) bv1[1] bv0[1]))
(let (?e67 (bvor ?e56 (zero_extend[3] ?e48)))
(let (?e68 (ite (= ?e36 ?e8) bv1[1] bv0[1]))
(flet ($e69 (bvsle ?e28 ?e13))
(flet ($e70 (bvsgt ?e51 (sign_extend[3] ?e17)))
(flet ($e71 (bvule (zero_extend[3] ?e66) ?e16))
(flet ($e72 (distinct (sign_extend[3] ?e29) ?e10))
(flet ($e73 (bvult ?e27 ?e62))
(flet ($e74 (bvsgt ?e62 ?e33))
(flet ($e75 (bvule ?e52 ?e67))
(flet ($e76 (bvsle ?e46 ?e24))
(flet ($e77 (bvsgt ?e64 ?e35))
(flet ($e78 (bvuge ?e19 (zero_extend[3] ?e41)))
(flet ($e79 (bvsge (sign_extend[3] ?e18) ?e33))
(flet ($e80 (bvuge ?e32 (zero_extend[3] ?e25)))
(flet ($e81 (bvslt ?e12 ?e36))
(flet ($e82 (= v3 ?e42))
(flet ($e83 (bvuge ?e54 ?e50))
(flet ($e84 (bvuge ?e67 ?e27))
(flet ($e85 (bvsge ?e37 (zero_extend[3] ?e26)))
(flet ($e86 (bvsle ?e54 (zero_extend[3] ?e38)))
(flet ($e87 (bvule (zero_extend[3] ?e40) ?e30))
(flet ($e88 (bvuge ?e54 ?e36))
(flet ($e89 (bvslt ?e10 ?e36))
(flet ($e90 (bvsgt ?e44 ?e61))
(flet ($e91 (distinct ?e59 ?e13))
(flet ($e92 (bvsle ?e65 ?e21))
(flet ($e93 (bvult v2 (zero_extend[3] ?e17)))
(flet ($e94 (bvsge ?e51 v2))
(flet ($e95 (bvslt ?e14 ?e30))
(flet ($e96 (bvult (zero_extend[3] ?e38) ?e21))
(flet ($e97 (bvugt ?e59 (zero_extend[3] ?e26)))
(flet ($e98 (bvugt ?e13 (zero_extend[2] ?e34)))
(flet ($e99 (= (zero_extend[3] ?e39) ?e7))
(flet ($e100 (= (sign_extend[3] ?e20) ?e10))
(flet ($e101 (bvsgt ?e13 ?e59))
(flet ($e102 (bvult (sign_extend[3] ?e41) ?e59))
(flet ($e103 (bvuge ?e52 ?e67))
(flet ($e104 (bvuge ?e8 ?e59))
(flet ($e105 (bvsgt ?e67 (zero_extend[3] ?e38)))
(flet ($e106 (bvsle (zero_extend[3] ?e29) ?e28))
(flet ($e107 (bvult ?e6 ?e24))
(flet ($e108 (bvult ?e12 v1))
(flet ($e109 (bvsle ?e7 ?e24))
(flet ($e110 (bvule ?e38 ?e47))
(flet ($e111 (bvugt (zero_extend[3] ?e60) ?e49))
(flet ($e112 (bvult ?e19 ?e55))
(flet ($e113 (bvuge ?e33 ?e55))
(flet ($e114 (bvslt ?e39 ?e31))
(flet ($e115 (distinct (zero_extend[3] ?e18) ?e56))
(flet ($e116 (bvult ?e45 v1))
(flet ($e117 (bvsgt ?e43 (sign_extend[3] ?e39)))
(flet ($e118 (bvsge ?e64 ?e68))
(flet ($e119 (bvsle v4 v1))
(flet ($e120 (distinct ?e56 (zero_extend[3] ?e61)))
(flet ($e121 (distinct ?e10 ?e7))
(flet ($e122 (bvsgt (sign_extend[3] ?e17) ?e52))
(flet ($e123 (bvsle ?e42 (zero_extend[3] ?e61)))
(flet ($e124 (bvsle ?e5 ?e13))
(flet ($e125 (bvule ?e38 ?e39))
(flet ($e126 (bvugt ?e9 ?e53))
(flet ($e127 (bvsgt ?e62 (sign_extend[3] ?e39)))
(flet ($e128 (bvsge ?e27 ?e24))
(flet ($e129 (bvuge (sign_extend[3] ?e48) ?e65))
(flet ($e130 (distinct ?e46 (zero_extend[3] ?e17)))
(flet ($e131 (bvsle (sign_extend[3] ?e47) ?e33))
(flet ($e132 (bvslt ?e36 ?e67))
(flet ($e133 (bvule v4 (sign_extend[3] ?e17)))
(flet ($e134 (distinct ?e13 (zero_extend[3] ?e31)))
(flet ($e135 (= ?e59 (sign_extend[3] ?e38)))
(flet ($e136 (bvsle ?e27 ?e28))
(flet ($e137 (bvsle v0 (sign_extend[3] ?e47)))
(flet ($e138 (bvule ?e65 (zero_extend[3] ?e11)))
(flet ($e139 (bvsgt ?e37 ?e16))
(flet ($e140 (bvugt ?e25 ?e60))
(flet ($e141 (bvuge ?e15 ?e7))
(flet ($e142 (= ?e58 ?e52))
(flet ($e143 (distinct ?e52 ?e23))
(flet ($e144 (bvsgt ?e30 ?e54))
(flet ($e145 (bvugt ?e6 ?e7))
(flet ($e146 (bvugt ?e45 ?e37))
(flet ($e147 (bvuge ?e62 ?e43))
(flet ($e148 (bvult (zero_extend[3] ?e18) ?e42))
(flet ($e149 (bvsgt ?e23 (zero_extend[3] ?e61)))
(flet ($e150 (bvslt (sign_extend[3] ?e40) ?e15))
(flet ($e151 (bvugt ?e28 (sign_extend[3] ?e11)))
(flet ($e152 (bvugt ?e25 ?e66))
(flet ($e153 (bvugt ?e28 ?e19))
(flet ($e154 (= ?e52 (zero_extend[3] ?e47)))
(flet ($e155 (bvuge ?e7 ?e16))
(flet ($e156 (bvult (zero_extend[3] ?e17) ?e43))
(flet ($e157 (bvsle (zero_extend[3] ?e60) ?e21))
(flet ($e158 (= ?e16 ?e27))
(flet ($e159 (bvsgt ?e12 (sign_extend[3] ?e35)))
(flet ($e160 (distinct ?e42 ?e19))
(flet ($e161 (bvult (zero_extend[3] ?e48) ?e14))
(flet ($e162 (bvsle ?e7 (sign_extend[3] ?e41)))
(flet ($e163 (bvuge ?e14 ?e13))
(flet ($e164 (distinct ?e14 v3))
(flet ($e165 (bvsle (zero_extend[3] ?e64) ?e65))
(flet ($e166 (bvule ?e7 ?e58))
(flet ($e167 (distinct ?e15 (sign_extend[3] ?e64)))
(flet ($e168 (bvuge ?e42 ?e30))
(flet ($e169 (bvule ?e8 v0))
(flet ($e170 (bvsge ?e50 ?e62))
(flet ($e171 (bvsgt v2 ?e58))
(flet ($e172 (bvsge ?e40 ?e44))
(flet ($e173 (bvsle ?e49 (sign_extend[3] ?e39)))
(flet ($e174 (bvule (sign_extend[3] ?e44) v1))
(flet ($e175 (bvugt ?e50 (zero_extend[3] ?e41)))
(flet ($e176 (bvule ?e66 ?e20))
(flet ($e177 (bvule ?e43 v3))
(flet ($e178 (distinct (sign_extend[3] ?e39) ?e50))
(flet ($e179 (bvslt ?e57 (zero_extend[3] ?e18)))
(flet ($e180 (bvsle ?e59 ?e23))
(flet ($e181 (bvule ?e13 ?e19))
(flet ($e182 (bvuge (sign_extend[3] ?e60) ?e55))
(flet ($e183 (bvult ?e56 ?e49))
(flet ($e184 (bvult (zero_extend[3] ?e11) ?e14))
(flet ($e185 (bvslt (zero_extend[3] ?e39) ?e52))
(flet ($e186 (bvslt ?e53 (sign_extend[3] ?e41)))
(flet ($e187 (bvule (zero_extend[3] ?e20) ?e33))
(flet ($e188 (distinct (zero_extend[3] ?e26) ?e12))
(flet ($e189 (bvult ?e8 v2))
(flet ($e190 (bvslt ?e8 ?e22))
(flet ($e191 (bvsge ?e9 ?e12))
(flet ($e192 (distinct (sign_extend[3] ?e39) ?e27))
(flet ($e193 (bvule ?e55 ?e15))
(flet ($e194 (bvsle ?e53 ?e37))
(flet ($e195 (bvule (sign_extend[3] ?e66) ?e14))
(flet ($e196 (bvugt ?e53 ?e57))
(flet ($e197 (bvsle v0 (zero_extend[3] ?e47)))
(flet ($e198 (bvugt ?e23 (sign_extend[3] ?e63)))
(flet ($e199 
(and
 (or $e103 $e102 (not $e168))
 (or (not $e149) (not $e88) (not $e180))
 (or (not $e126) $e179 (not $e114))
 (or $e197 $e131 (not $e132))
 (or (not $e143) (not $e107) $e156)
 (or (not $e181) $e120 $e109)
 (or $e135 (not $e78) $e163)
 (or $e198 $e187 $e100)
 (or (not $e128) (not $e138) $e192)
 (or $e181 $e161 (not $e186))
 (or $e153 $e167 $e182)
 (or (not $e94) (not $e151) $e164)
 (or $e104 (not $e72) $e157)
 (or $e159 $e141 $e183)
 (or $e191 $e147 (not $e79))
 (or (not $e71) $e138 (not $e183))
 (or (not $e184) $e184 $e143)
 (or (not $e145) $e193 (not $e136))
 (or (not $e196) $e160 $e91)
 (or $e130 $e152 (not $e177))
 (or $e174 (not $e95) (not $e111))
 (or (not $e165) $e163 $e196)
 (or $e69 (not $e183) (not $e187))
 (or (not $e169) $e112 (not $e174))
 (or $e109 $e76 (not $e141))
 (or (not $e119) (not $e170) $e112)
 (or (not $e172) (not $e122) (not $e108))
 (or (not $e143) $e95 (not $e118))
 (or (not $e156) (not $e172) $e97)
 (or $e188 (not $e169) $e85)
 (or (not $e115) (not $e135) $e158)
 (or (not $e133) $e134 $e71)
 (or $e129 (not $e102) (not $e124))
 (or (not $e180) (not $e181) $e81)
 (or (not $e161) (not $e82) (not $e102))
 (or (not $e148) (not $e167) (not $e91))
 (or (not $e161) (not $e90) $e104)
 (or (not $e178) $e180 $e165)
 (or (not $e151) (not $e81) (not $e81))
 (or $e128 (not $e156) $e197)
 (or (not $e125) (not $e123) $e125)
 (or (not $e76) $e141 (not $e126))
 (or (not $e122) (not $e94) $e139)
 (or $e122 $e109 $e101)
 (or $e104 (not $e170) (not $e92))
 (or (not $e122) $e180 $e105)
 (or $e169 $e78 (not $e114))
 (or (not $e161) $e95 $e73)
 (or (not $e93) (not $e144) (not $e169))
 (or (not $e135) $e85 $e144)
 (or $e121 $e197 $e189)
 (or $e131 $e162 $e154)
 (or $e163 $e84 $e135)
 (or $e122 $e191 $e167)
 (or (not $e105) (not $e90) $e71)
 (or $e171 $e163 $e153)
 (or (not $e141) (not $e164) (not $e146))
 (or (not $e140) $e155 (not $e164))
 (or (not $e118) (not $e135) $e78)
 (or (not $e127) $e175 (not $e100))
 (or $e196 $e81 (not $e116))
 (or (not $e100) $e195 $e85)
 (or (not $e159) (not $e112) (not $e168))
 (or $e120 (not $e173) (not $e155))
 (or $e198 (not $e77) $e165)
))
$e199
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))