; COMMAND-LINE: --bv-to-bool
; EXPECT: sat
(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun v1 () (_ BitVec 2))
(declare-fun v2 () (_ BitVec 11))
(declare-fun v3 () (_ BitVec 5))
(declare-fun v4 () (_ BitVec 15))
(check-sat-assuming ( (let ((_let_0 (ite (bvult v4 ((_ sign_extend 13) v1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 ((_ sign_extend 9) v1))) (let ((_let_2 (bvcomp v4 v4))) (let ((_let_3 (bvadd (bvadd _let_1 v2) ((_ zero_extend 10) _let_0)))) (let ((_let_4 (bvand v0 ((_ sign_extend 11) v3)))) (let ((_let_5 ((_ repeat 1) v0))) (let ((_let_6 (ite (bvsge v4 ((_ zero_extend 14) _let_0)) (_ bv1 1) (_ bv0 1)))) (let ((_let_7 (ite (bvule _let_4 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_8 (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) _let_3))) (let ((_let_9 ((_ sign_extend 10) _let_2))) (let ((_let_10 (= (or (or (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) _let_3) (= ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) v0)) (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (or (or (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) _let_3) (= ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) v0)) (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (let ((_let_11 (or (or (or (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3)))))) (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))))))) (or (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3)))))) (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3)))))))) (or (or (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3)))))) (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))))))) (or (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3)))))) (xor (= (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))))))) (= (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))) (ite (= (and (and (=> (= (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) v2) (= v0 ((_ zero_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))) (= v4 ((_ zero_extend 14) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (and (= (_ bv0 1) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (and (= _let_3 _let_9) (= _let_2 (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))) (= (bvadd _let_1 v2) ((_ sign_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)))))) (= (= (bvadd _let_1 v2) (bvadd _let_1 v2)) (= ((_ zero_extend 4) _let_0) v3))) (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)))) (= (= (or (not (= v3 ((_ sign_extend 4) _let_6))) (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (=> (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (=> (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= v0 ((_ sign_extend 15) _let_6))))) (and (not (xor (ite (= ((_ zero_extend 14) _let_6) v4) (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_0) (not (= ((_ zero_extend 10) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (xor (= (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)) _let_2) (= (= (= (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1)) _let_7) (or (= (bvadd _let_1 v2) _let_9) (ite (not _let_8) (= ((_ sign_extend 10) (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) _let_3) (not (= ((_ zero_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) ((_ sign_extend 6) v3)))))) (and (= _let_7 _let_7) (= ((_ sign_extend 4) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) v4)))) (not (= (=> (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0))) (and (=> (= ((_ zero_extend 15) _let_6) _let_4) (= ((_ zero_extend 15) _let_6) _let_4)) (= v1 ((_ sign_extend 1) _let_0)))) (= v4 ((_ sign_extend 14) (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))))))))) (and (= (= (ite (=> (ite (= ((_ zero_extend 15) _let_7) v0) (= (xor (= _let_6 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (= ((_ sign_extend 15) _let_2) v0)) (not (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))))) (or (not (not (or (= (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))) (_ bv0 1)) (= ((_ zero_extend 10) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_3)))) (xor (= v1 ((_ sign_extend 1) (_ bv0 1))) (= _let_6 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))))) (ite (= _let_7 _let_6) (or _let_8 (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_6 _let_0))) (= ((_ sign_extend 15) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) _let_4) (not (= (bvcomp ((_ sign_extend 10) _let_0) _let_3) _let_2))) (=> (not (= v1 ((_ sign_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))) (= ((_ sign_extend 10) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) (bvadd _let_1 v2)))) (not (= (= (_ bv0 1) (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1))) (= _let_6 _let_7)))) (= (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))) (or (ite (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1))))))) (ite (ite (= (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) (= _let_7 _let_6) (and (=> (= ((_ zero_extend 1) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))) v1) (= _let_4 ((_ sign_extend 15) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))))) (or (= ((_ sign_extend 14) _let_7) v4) (and (= ((_ sign_extend 13) v1) v4) (= ((_ zero_extend 10) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (bvadd _let_1 v2)))))) (= ((_ zero_extend 4) (bvcomp ((_ sign_extend 10) _let_0) _let_3)) v3) (= ((_ sign_extend 15) _let_7) _let_4)) (ite (=> (= _let_7 (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1))) (ite (= _let_7 (ite (bvsge ((_ zero_extend 11) v3) v0) (_ bv1 1) (_ bv0 1))) (= v4 ((_ zero_extend 14) (bvcomp ((_ sign_extend 10) _let_0) _let_3))) (= v0 ((_ zero_extend 5) _let_3)))) (= (= _let_6 _let_0) (= ((_ sign_extend 1) v4) _let_5)) (= (xor (= _let_3 _let_1) (= (ite (bvsle (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0)) (ite (= (_ bv1 1) ((_ extract 0 0) v0)) _let_3 ((_ zero_extend 10) _let_0))) (_ bv1 1) (_ bv0 1)) (ite (bvsle _let_1 v2) (_ bv1 1) (_ bv0 1)))) (= _let_5 ((_ zero_extend 15) (bvshl _let_0 (ite (bvsge ((_ zero_extend 9) v1) _let_3) (_ bv1 1) (_ bv0 1)))))))) (= _let_4 ((_ sign_extend 5) _let_3))))))))))) (= (=> _let_11 _let_11) (not (not (or _let_10 _let_10)))))))))))))))) ))