(set-option :incremental false)
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun v1 () (_ BitVec 7))
(declare-fun v2 () (_ BitVec 15))
(assert (let ((_let_0 (ite (bvugt ((_ sign_extend 6) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1))) v1) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (bvudiv _let_0 _let_0))) (let ((_let_2 (ite (bvsle _let_1 (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_3 ((_ zero_extend 14) _let_2))) (let ((_let_4 (bvslt _let_2 _let_1))) (let ((_let_5 ((_ sign_extend 15) _let_0))) (let ((_let_6 (ite (bvugt v0 ((_ zero_extend 15) _let_0)) (bvult (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)) _let_0) (xor (distinct _let_2 (ite (distinct (_ bv31209 16) ((_ zero_extend 15) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))) (xor (= (bvsgt _let_0 _let_0) (bvult _let_3 v2)) (bvsgt ((_ zero_extend 1) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) ((_ sign_extend 1) _let_1))))))) (let ((_let_7 (ite (not (bvsle (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)) _let_1)) (= v0 ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1)))) (bvsle v1 ((_ zero_extend 6) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1))))))) (let ((_let_8 (not (xor (bvuge (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)) _let_0) (bvule ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0))))) (and (and (=> _let_8 _let_8) (not (not (ite (bvugt (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1))) (bvugt v1 ((_ zero_extend 6) (ite (distinct (_ bv31209 16) ((_ zero_extend 15) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (= (xor (not (ite (not (bvuge _let_5 v0)) (bvslt ((_ sign_extend 1) _let_1) ((_ sign_extend 1) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)))) (and _let_4 (bvslt v1 ((_ sign_extend 6) (ite (distinct (_ bv31209 16) ((_ zero_extend 15) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))))) (or (bvugt (ite (distinct (_ bv31209 16) ((_ zero_extend 15) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ sign_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v0) (_ bv1 1) (_ bv0 1))) _let_4)) (=> (xor _let_7 _let_7) (or (xor (=> (bvslt ((_ sign_extend 6) (ite (bvsgt (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1)) _let_1) (_ bv1 1) (_ bv0 1))) v1) (bvule (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1)) _let_1)) (bvsle ((_ zero_extend 6) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) v1)) (or (or (and (and (bvsle _let_0 (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1))) (distinct (_ bv31209 16) ((_ zero_extend 15) _let_0))) (= (bvsle v0 _let_5) (and (bvule v2 v2) (bvuge ((_ sign_extend 8) v1) v2)))) (or (bvuge (_ bv31209 16) ((_ zero_extend 15) (ite (bvsle v2 v2) (_ bv1 1) (_ bv0 1)))) (distinct v2 _let_3))) (ite _let_6 (= v2 _let_3) _let_6))))))))) (not (= _let_0 (_ bv0 1))))))))))))))
(check-sat)