z3: sat, yices2: unsat, cvc4: unsat

incorrect.smt2

(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 35))
(declare-fun v1 () (_ BitVec 70))
(assert (let ((e2(_ bv6766491 27)))
(let ((e3(_ bv168620854680901873565 68)))
(let ((e4 (ite (bvsle e3 ((_ zero_extend 33) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e5 (bvudiv ((_ sign_extend 67) e4) e3)))
(let ((e6 ((_ rotate_left 6) e2)))
(let ((e7 ((_ extract 23 6) v0)))
(let ((e8 ((_ repeat 4) e6)))
(let ((e9 (concat e6 v0)))
(let ((e10 (concat e4 e5)))
(let ((e11 (bvlshr ((_ zero_extend 51) e7) e10)))
(let ((e12 (ite (bvsle ((_ sign_extend 40) e3) e8) (_ bv1 1) (_ bv0 1))))
(let ((e13 ((_ rotate_right 50) e11)))
(let ((e14 (ite (bvuge ((_ zero_extend 67) e4) e5) (_ bv1 1) (_ bv0 1))))
(let ((e15 (ite (bvule ((_ sign_extend 26) e14) e6) (_ bv1 1) (_ bv0 1))))
(let ((e16 (bvneg e9)))
(let ((e17 (bvsub e8 ((_ zero_extend 39) e10))))
(let ((e18 (bvor ((_ zero_extend 35) e2) e16)))
(let ((e19 (bvcomp e18 e9)))
(let ((e20 (bvxnor ((_ zero_extend 68) e15) e10)))
(let ((e21 (bvand v0 v0)))
(let ((e22 ((_ extract 50 35) e18)))
(let ((e23 (ite (bvult e13 ((_ zero_extend 34) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e24 (ite (bvslt e5 ((_ sign_extend 67) e15)) (_ bv1 1) (_ bv0 1))))
(let ((e25 (bvor ((_ zero_extend 46) e18) e8)))
(let ((e26 (bvsdiv ((_ zero_extend 68) e15) e13)))
(let ((e27 (bvand e11 e26)))
(let ((e28 (concat e3 e19)))
(let ((e29 (ite (= (_ bv1 1) ((_ extract 17 17) v0)) e10 e27)))
(let ((e30 ((_ sign_extend 51) e20)))
(let ((e31 (bvshl e7 ((_ sign_extend 17) e23))))
(let ((e32 (ite (bvsge e9 ((_ sign_extend 61) e12)) (_ bv1 1) (_ bv0 1))))
(let ((e33 (bvlshr ((_ zero_extend 41) e6) e5)))
(let ((e34 (bvnot v0)))
(let ((e35 (ite (bvugt e21 ((_ sign_extend 17) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e36 (bvmul e29 ((_ sign_extend 1) e3))))
(let ((e37 ((_ extract 5 2) v0)))
(let ((e38 (bvashr e17 ((_ zero_extend 40) e33))))
(let ((e39 ((_ sign_extend 50) e11)))
(let ((e40 (bvnand e18 ((_ sign_extend 35) e6))))
(let ((e41 ((_ extract 57 34) e28)))
(let ((e42 (ite (bvuge e10 ((_ zero_extend 68) e15)) (_ bv1 1) (_ bv0 1))))
(let ((e43 (ite (= ((_ zero_extend 67) e23) e33) (_ bv1 1) (_ bv0 1))))
(let ((e44 (bvadd e39 e39)))
(let ((e45 (bvnor v1 ((_ sign_extend 69) e42))))
(let ((e46 (bvuge ((_ sign_extend 119) e42) e30)))
(let ((e47 (bvuge ((_ zero_extend 34) e43) e21)))
(let ((e48 (bvsgt v0 ((_ sign_extend 34) e32))))
(let ((e49 (bvuge e39 ((_ sign_extend 118) e35))))
(let ((e50 (distinct ((_ sign_extend 107) e15) e17)))
(let ((e51 (bvult e40 ((_ sign_extend 38) e41))))
(let ((e52 (bvsge e25 ((_ sign_extend 39) e26))))
(let ((e53 (bvugt e20 ((_ zero_extend 65) e37))))
(let ((e54 (bvsgt ((_ sign_extend 1) e20) e45)))
(let ((e55 (= ((_ zero_extend 58) e16) e30)))
(let ((e56 (bvsle ((_ sign_extend 68) e35) e28)))
(let ((e57 (bvslt e44 ((_ zero_extend 118) e12))))
(let ((e58 (= ((_ sign_extend 68) e35) e28)))
(let ((e59 (bvsgt e14 e12)))
(let ((e60 (bvsgt ((_ sign_extend 34) e34) e29)))
(let ((e61 (bvugt e22 ((_ sign_extend 15) e4))))
(let ((e62 (bvsle ((_ zero_extend 1) e13) e45)))
(let ((e63 (distinct e3 ((_ sign_extend 67) e14))))
(let ((e64 (bvugt e9 ((_ sign_extend 61) e14))))
(let ((e65 (bvule ((_ zero_extend 67) e15) e3)))
(let ((e66 (bvsge e26 ((_ sign_extend 68) e19))))
(let ((e67 (bvsgt v1 ((_ sign_extend 69) e12))))
(let ((e68 (bvult e45 v1)))
(let ((e69 (bvule ((_ sign_extend 11) e17) e39)))
(let ((e70 (bvuge ((_ zero_extend 73) e34) e38)))
(let ((e71 (bvsgt ((_ sign_extend 118) e35) e44)))
(let ((e72 (= ((_ sign_extend 26) e19) e6)))
(let ((e73 (= ((_ sign_extend 2) e5) v1)))
(let ((e74 (bvuge e34 e34)))
(let ((e75 (bvslt ((_ sign_extend 34) e21) e11)))
(let ((e76 (distinct e36 ((_ sign_extend 68) e42))))
(let ((e77 (distinct ((_ sign_extend 1) e33) e29)))
(let ((e78 (bvsle e29 e13)))
(let ((e79 (bvsle e28 ((_ zero_extend 68) e12))))
(let ((e80 (distinct ((_ zero_extend 67) e12) e33)))
(let ((e81 (bvsge e17 ((_ sign_extend 81) e6))))
(let ((e82 (bvsgt e25 ((_ zero_extend 73) e21))))
(let ((e83 (bvule ((_ zero_extend 68) e14) e13)))
(let ((e84 (bvuge ((_ zero_extend 26) e19) e6)))
(let ((e85 (bvsge ((_ sign_extend 27) v0) e16)))
(let ((e86 (= e5 ((_ sign_extend 50) e31))))
(let ((e87 (bvugt ((_ sign_extend 38) e41) e18)))
(let ((e88 (bvuge e3 ((_ zero_extend 52) e22))))
(let ((e89 (bvuge ((_ sign_extend 1) e3) e10)))
(let ((e90 (distinct e16 e9)))
(let ((e91 (bvslt ((_ zero_extend 54) e22) e45)))
(let ((e92 (bvuge e30 ((_ zero_extend 51) e28))))
(let ((e93 (bvslt e25 ((_ sign_extend 40) e3))))
(let ((e94 (bvuge ((_ zero_extend 50) e13) e39)))
(let ((e95 (= e16 ((_ zero_extend 61) e35))))
(let ((e96 (bvugt ((_ zero_extend 31) e37) v0)))
(let ((e97 (bvsge e14 e32)))
(let ((e98 (bvugt e25 ((_ zero_extend 107) e24))))
(let ((e99 (bvuge ((_ zero_extend 68) e15) e26)))
(let ((e100 (bvuge ((_ sign_extend 34) e14) v0)))
(let ((e101 (bvuge e21 ((_ zero_extend 19) e22))))
(let ((e102 (bvsge ((_ zero_extend 50) e27) e44)))
(let ((e103 (bvsgt ((_ zero_extend 58) e37) e18)))
(let ((e104 (bvsle ((_ sign_extend 107) e19) e38)))
(let ((e105 (bvsgt e16 ((_ sign_extend 27) e34))))
(let ((e106 (bvugt ((_ sign_extend 8) e40) e45)))
(let ((e107 (bvult e32 e42)))
(let ((e108 (bvugt ((_ sign_extend 39) e20) e8)))
(let ((e109 (distinct e26 ((_ sign_extend 68) e15))))
(let ((e110 (bvsge e34 ((_ sign_extend 34) e12))))
(let ((e111 (bvsgt e24 e35)))
(let ((e112 (bvslt e23 e35)))
(let ((e113 (bvslt e44 ((_ zero_extend 103) e22))))
(let ((e114 (= ((_ sign_extend 119) e12) e30)))
(let ((e115 (distinct e30 ((_ sign_extend 51) e20))))
(let ((e116 (bvsge ((_ zero_extend 107) e43) e38)))
(let ((e117 (= ((_ sign_extend 68) e4) e27)))
(let ((e118 (= ((_ zero_extend 46) e16) e38)))
(let ((e119 (bvsle ((_ sign_extend 58) e18) e30)))
(let ((e120 (bvsle e21 ((_ sign_extend 34) e23))))
(let ((e121 (= ((_ zero_extend 3) e35) e37)))
(let ((e122 (bvuge e7 ((_ sign_extend 17) e43))))
(let ((e123 (bvsge e13 ((_ zero_extend 34) e21))))
(let ((e124 (bvugt ((_ zero_extend 68) e24) e27)))
(let ((e125 (distinct ((_ zero_extend 115) e37) e39)))
(let ((e126 (bvult e13 ((_ sign_extend 68) e43))))
(let ((e127 (bvult e8 ((_ sign_extend 38) v1))))
(let ((e128 (= e39 ((_ sign_extend 118) e43))))
(let ((e129 (bvuge e28 ((_ zero_extend 7) e18))))
(let ((e130 (bvsge ((_ sign_extend 34) e21) e29)))
(let ((e131 (bvult e20 ((_ sign_extend 7) e18))))
(let ((e132 (distinct e11 ((_ zero_extend 42) e6))))
(let ((e133 (bvsle e20 ((_ sign_extend 68) e24))))
(let ((e134 (bvsgt ((_ zero_extend 33) e21) e3)))
(let ((e135 (bvugt e45 ((_ sign_extend 35) v0))))
(let ((e136 (= e18 ((_ zero_extend 44) e31))))
(let ((e137 (bvugt ((_ zero_extend 107) e14) e17)))
(let ((e138 (bvsle v0 ((_ zero_extend 34) e4))))
(let ((e139 (bvuge e28 e20)))
(let ((e140 (bvuge e11 ((_ sign_extend 51) e7))))
(let ((e141 (distinct e44 e39)))
(let ((e142 (bvsle ((_ zero_extend 35) e2) e16)))
(let ((e143 (not e97)))
(let ((e144 (and e95 e69)))
(let ((e145 (ite e96 e65 e106)))
(let ((e146 (or e143 e53)))
(let ((e147 (ite e77 e107 e90)))
(let ((e148 (or e119 e47)))
(let ((e149 (= e103 e98)))
(let ((e150 (or e85 e135)))
(let ((e151 (not e118)))
(let ((e152 (not e64)))
(let ((e153 (not e75)))
(let ((e154 (and e121 e78)))
(let ((e155 (=> e139 e146)))
(let ((e156 (and e86 e49)))
(let ((e157 (=> e142 e84)))
(let ((e158 (and e111 e72)))
(let ((e159 (not e158)))
(let ((e160 (and e117 e136)))
(let ((e161 (or e67 e155)))
(let ((e162 (=> e48 e70)))
(let ((e163 (not e76)))
(let ((e164 (and e152 e163)))
(let ((e165 (or e83 e115)))
(let ((e166 (not e56)))
(let ((e167 (not e46)))
(let ((e168 (ite e112 e66 e99)))
(let ((e169 (or e54 e58)))
(let ((e170 (= e50 e91)))
(let ((e171 (= e105 e165)))
(let ((e172 (ite e171 e114 e137)))
(let ((e173 (ite e162 e108 e73)))
(let ((e174 (and e132 e122)))
(let ((e175 (or e89 e63)))
(let ((e176 (or e109 e59)))
(let ((e177 (xor e104 e172)))
(let ((e178 (and e74 e80)))
(let ((e179 (xor e174 e169)))
(let ((e180 (xor e94 e157)))
(let ((e181 (=> e131 e170)))
(let ((e182 (= e176 e101)))
(let ((e183 (=> e149 e141)))
(let ((e184 (ite e57 e81 e148)))
(let ((e185 (or e145 e138)))
(let ((e186 (not e129)))
(let ((e187 (= e167 e82)))
(let ((e188 (not e147)))
(let ((e189 (not e88)))
(let ((e190 (xor e160 e110)))
(let ((e191 (not e188)))
(let ((e192 (not e87)))
(let ((e193 (ite e79 e185 e186)))
(let ((e194 (= e61 e126)))
(let ((e195 (not e123)))
(let ((e196 (or e179 e194)))
(let ((e197 (ite e150 e62 e164)))
(let ((e198 (xor e113 e144)))
(let ((e199 (and e133 e189)))
(let ((e200 (and e180 e151)))
(let ((e201 (or e190 e55)))
(let ((e202 (or e168 e71)))
(let ((e203 (= e175 e93)))
(let ((e204 (= e187 e60)))
(let ((e205 (xor e161 e197)))
(let ((e206 (not e204)))
(let ((e207 (xor e153 e166)))
(let ((e208 (not e207)))
(let ((e209 (and e201 e124)))
(let ((e210 (or e205 e100)))
(let ((e211 (=> e128 e51)))
(let ((e212 (ite e184 e199 e116)))
(let ((e213 (ite e211 e208 e127)))
(let ((e214 (and e52 e210)))
(let ((e215 (= e214 e159)))
(let ((e216 (or e202 e202)))
(let ((e217 (= e177 e134)))
(let ((e218 (and e181 e195)))
(let ((e219 (xor e198 e209)))
(let ((e220 (xor e102 e200)))
(let ((e221 (xor e140 e196)))
(let ((e222 (=> e213 e130)))
(let ((e223 (and e215 e215)))
(let ((e224 (or e212 e220)))
(let ((e225 (or e154 e120)))
(let ((e226 (=> e125 e223)))
(let ((e227 (= e222 e156)))
(let ((e228 (xor e217 e182)))
(let ((e229 (=> e216 e218)))
(let ((e230 (and e92 e173)))
(let ((e231 (= e224 e224)))
(let ((e232 (not e206)))
(let ((e233 (not e68)))
(let ((e234 (or e229 e228)))
(let ((e235 (not e221)))
(let ((e236 (not e232)))
(let ((e237 (xor e230 e234)))
(let ((e238 (or e178 e193)))
(let ((e239 (=> e235 e191)))
(let ((e240 (ite e227 e183 e203)))
(let ((e241 (=> e225 e231)))
(let ((e242 (xor e238 e237)))
(let ((e243 (= e240 e242)))
(let ((e244 (= e236 e243)))
(let ((e245 (not e241)))
(let ((e246 (= e233 e245)))
(let ((e247 (and e219 e246)))
(let ((e248 (not e239)))
(let ((e249 (or e248 e248)))
(let ((e250 (ite e247 e226 e244)))
(let ((e251 (= e249 e249)))
(let ((e252 (and e250 e250)))
(let ((e253 (not e192)))
(let ((e254 (= e253 e252)))
(let ((e255 (and e251 e254)))
(let ((e256 (and e255 (not (= e13 (_ bv0 69))))))
(let ((e257 (and e256 (not (= e13 (bvnot (_ bv0 69)))))))
(let ((e258 (and e257 (not (= e3 (_ bv0 68))))))
e258
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)

Thanks, fixed