(set-logic QF_BV)
(set-info :smt-lib-version 2.0)
(set-info :category "unknown")
(set-info :status sat)
(declare-fun v0 () (_ BitVec 12))
(declare-fun v1 () (_ BitVec 1))
(assert (let ((?v_0 ((_ extract 8 8) v0))) (let ((?v_1 (ite (bvsle v1 ?v_0) (_ bv1 1) (_ bv0 1)))) (let ((?v_12 (ite (= (_ bv1 1) ((_ extract 0 0) v1)) ?v_1 ?v_0)) (?v_2 (ite (bvult v1 ?v_1) (_ bv1 1) (_ bv0 1))) (?v_3 (bvsub v0 v0))) (let ((?v_4 (ite (bvsle ((_ sign_extend 11) ?v_0) ?v_3) (_ bv1 1) (_ bv0 1))) (?v_16 (ite (bvult ?v_3 ((_ sign_extend 11) v1)) (_ bv1 1) (_ bv0 1))) (?v_8 (bvnot (_ bv28 5)))) (let ((?v_9 (bvshl ?v_16 ?v_4)) (?v_5 (bvneg ?v_1)) (?v_13 (concat ?v_8 (_ bv28 5)))) (let ((?v_10 (bvxor ?v_5 ?v_2)) (?v_15 (bvcomp ?v_2 ?v_9)) (?v_14 (ite (bvsle ?v_0 ?v_9) (_ bv1 1) (_ bv0 1)))) (let ((?v_11 (ite (bvsle ?v_0 ?v_14) (_ bv1 1) (_ bv0 1))) (?v_26 (bvudiv ?v_4 ?v_12)) (?v_7 ((_ repeat 7) (_ bv1 1))) (?v_24 (bvslt (_ bv1 1) (_ bv1 1))) (?v_6 (bvslt ?v_5 v1)) (?v_18 ((_ sign_extend 4) ?v_4)) (?v_19 ((_ sign_extend 4) ?v_5)) (?v_27 ((_ sign_extend 6) ?v_10)) (?v_23 (bvule ?v_10 ?v_10)) (?v_22 (bvult ?v_13 ((_ sign_extend 9) ?v_5)))) (let ((?v_20 (= (bvult ?v_8 ((_ zero_extend 4) ?v_11)) (bvsle ?v_1 ?v_14))) (?v_17 (=> (bvult ?v_1 ?v_16) (bvsle ?v_9 ?v_5)))) (let ((?v_21 (ite (or (= ?v_7 ((_ sign_extend 6) ?v_26)) (xor (=> (bvslt ?v_8 ((_ sign_extend 4) ?v_2)) (= ?v_2 ?v_15)) (bvule ?v_10 v1))) (bvult ((_ sign_extend 4) v1) (_ bv28 5)) (ite (ite (not (and ?v_6 ?v_6)) (and (=> (bvsle ((_ zero_extend 6) ?v_0) ?v_7) (bvult ?v_7 ((_ zero_extend 2) (_ bv28 5)))) (bvult ?v_13 ((_ zero_extend 9) ?v_9))) (or (or (bvslt ?v_19 (_ bv28 5)) (= (=> (= (bvsle ?v_1 ?v_11) (or (bvult ?v_8 ?v_18) (bvule ?v_27 ?v_7))) (bvsle ?v_11 ?v_12)) (or (or (bvslt (_ bv28 5) (_ bv28 5)) (distinct ?v_13 ((_ sign_extend 9) ?v_12))) (=> (bvult ((_ zero_extend 4) ?v_12) (_ bv28 5)) (bvslt ((_ sign_extend 6) ?v_14) ?v_7))))) (and (ite (bvslt ?v_12 ?v_12) (bvule ?v_3 v0) (= ?v_13 ((_ zero_extend 9) ?v_5))) (=> (bvsle ?v_15 ?v_4) (distinct ?v_8 ?v_8))))) (= (not (or ?v_17 ?v_17)) (and ?v_24 (or (bvslt ?v_18 ?v_8) (bvslt (_ bv28 5) ?v_19)))) (xor ?v_20 ?v_20))))) (let ((?v_25 (ite ?v_21 ?v_21 (xor (=> (bvslt ((_ sign_extend 9) ?v_9) ?v_13) (not (= (or ?v_22 ?v_22) (bvule ?v_3 ((_ zero_extend 11) ?v_10))))) (=> (and (ite (bvult (_ bv1 1) ?v_15) (bvslt ?v_5 (_ bv1 1)) (or ?v_23 ?v_23)) (= (bvsle ?v_0 ?v_16) (and (bvslt ((_ sign_extend 5) ?v_7) v0) ?v_24))) (bvsle ?v_1 ?v_4)))))) (and (or (or ?v_25 ?v_25) (= (not (xor (=> (= (bvsle ((_ zero_extend 11) ?v_4) ?v_3) (=> (or (xor (and (=> (bvule ((_ sign_extend 11) ?v_10) v0) (bvsle v1 v1)) (and (bvslt ?v_16 ?v_26) (not (bvsle ?v_7 ?v_27)))) (xor (bvult ?v_7 ?v_27) (= ?v_5 ?v_12))) (bvule (_ bv1 1) ?v_26)) (ite (bvule ((_ zero_extend 9) ?v_2) ?v_13) (bvslt ?v_7 ((_ sign_extend 6) (ite (bvsle (_ bv28 5) ((_ sign_extend 4) ?v_0)) (_ bv1 1) (_ bv0 1)))) (bvslt ?v_8 ((_ sign_extend 4) ?v_26))))) (bvule ((_ sign_extend 6) ?v_2) ?v_7)) (and (bvslt ((_ sign_extend 9) ?v_11) ?v_13) (=> (= (bvsle ?v_1 ?v_1) (bvult ?v_10 ?v_4)) (xor (= ?v_15 ?v_16) (bvult v0 ((_ sign_extend 11) ?v_14))))))) (not (bvslt ?v_14 ?v_0)))) (not (= ?v_12 (_ bv0 1)))))))))))))))
(check-sat)
(exit)