(set-info :status sat)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 13))
(declare-fun v1 () (_ BitVec 11))
(declare-fun v2 () (_ BitVec 15))
(declare-fun v3 () (_ BitVec 15))
(declare-fun v4 () (_ BitVec 11))
(assert (let ((_let_0 (ite (= (_ bv1 1) (bvnot (ite (= v3 (concat (_ bv0 4) v1)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (concat (_ bv0 10) (bvand (_ bv0 1) (bvnot (_ bv1 1)))))) (let ((_let_2 ((_ extract 10 10) _let_1))) (let ((_let_3 ((_ extract 10 10) v1))) (let ((_let_4 (ite (bvult ((_ extract 9 0) _let_1) ((_ extract 9 0) v1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_5 (bvnot _let_3))) (let ((_let_6 (bvand (bvnot (_ bv2 4)) (bvnot (concat (_ bv0 3) _let_0))))) (let ((_let_7 (concat (ite (= (_ bv1 1) ((_ extract 0 0) (bvand (_ bv0 1) (bvnot (_ bv1 1))))) (_ bv7 3) (_ bv0 3)) (bvand (_ bv0 1) (bvnot (_ bv1 1)))))) (let ((_let_8 ((_ extract 3 3) _let_7))) (let ((_let_9 ((_ extract 3 3) (_ bv2 4)))) (let ((_let_10 (ite (bvult ((_ extract 2 0) _let_7) ((_ extract 2 0) (_ bv2 4))) (_ bv1 1) (_ bv0 1)))) (let ((_let_11 (bvnot _let_9))) (let ((_let_12 (ite (= (_ bv1 1) (bvnot (bvand (bvnot (bvand _let_8 _let_11)) (bvand (bvnot (bvand (bvand (bvnot _let_8) _let_11) _let_10)) (bvnot (bvand (bvand _let_8 _let_9) _let_10)))))) (_ bv1 1) (_ bv0 1)))) (let ((_let_13 (= (_ bv1 1) ((_ extract 0 0) _let_0)))) (let ((_let_14 (bvadd _let_6 _let_6))) (let ((_let_15 (concat (_ bv0 1) _let_0))) (let ((_let_16 (ite (= (_ bv1 1) (bvnot (ite (= (concat (_ bv0 12) (_ bv0 1)) v0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)))) (let ((_let_17 (ite (= (_ bv1 1) (ite (= (concat (_ bv0 4) v1) v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (let ((_let_18 (concat ((_ extract 1 0) _let_6) ((_ extract 3 2) _let_6)))) (let ((_let_19 (concat (ite (= (_ bv1 1) ((_ extract 0 0) _let_16)) (_ bv7 3) (_ bv0 3)) _let_16))) (let ((_let_20 ((_ extract 3 3) _let_19))) (let ((_let_21 (ite (bvult ((_ extract 2 0) (_ bv2 4)) ((_ extract 2 0) _let_19)) (_ bv1 1) (_ bv0 1)))) (let ((_let_22 (bvnot _let_20))) (let ((_let_23 (concat (ite (= (_ bv1 1) ((_ extract 0 0) (bvand (_ bv0 1) (bvnot (_ bv1 1))))) (_ bv1 1) (_ bv0 1)) (bvand (_ bv0 1) (bvnot (_ bv1 1)))))) (let ((_let_24 ((_ extract 1 1) _let_15))) (let ((_let_25 ((_ extract 1 1) _let_23))) (let ((_let_26 (ite (bvult ((_ extract 0 0) _let_15) ((_ extract 0 0) _let_23)) (_ bv1 1) (_ bv0 1)))) (let ((_let_27 (bvnot _let_25))) (let ((_let_28 (concat (ite (= (_ bv1 1) ((_ extract 3 3) _let_18)) (_ bv511 9) (_ bv0 9)) _let_18))) (let ((_let_29 ((_ extract 12 12) v0))) (let ((_let_30 ((_ extract 12 12) _let_28))) (let ((_let_31 (ite (bvult ((_ extract 11 0) v0) ((_ extract 11 0) _let_28)) (_ bv1 1) (_ bv0 1)))) (let ((_let_32 (bvnot _let_30))) (let ((_let_33 ((_ zero_extend 2) ((_ extract 1 0) (concat (ite (= (_ bv1 1) ((_ extract 0 0) _let_17)) (_ bv7 3) (_ bv0 3)) _let_17))))) (let ((_let_34 (ite (= (_ bv1 1) (bvnot (ite (= ((_ extract 3 2) (concat (ite (= (_ bv1 1) ((_ extract 0 0) _let_17)) (_ bv7 3) (_ bv0 3)) _let_17)) (_ bv0 2)) (_ bv1 1) (_ bv0 1)))) (concat (ite (= (_ bv1 1) ((_ extract 0 0) ((_ extract 3 3) _let_18))) (_ bv7 3) (_ bv0 3)) ((_ extract 3 3) _let_18)) (ite (= (_ bv1 1) ((_ extract 3 3) _let_18)) (bvnot (bvlshr (bvnot _let_18) _let_33)) (bvlshr _let_18 _let_33))))) (let ((_let_35 (ite (bvult ((_ extract 2 0) _let_18) ((_ extract 2 0) _let_18)) (_ bv1 1) (_ bv0 1)))) (let ((_let_36 (concat (_ bv0 3) (ite (= (_ bv1 1) (ite (= (ite (= (_ bv1 1) (bvnot (ite (= ((_ extract 10 4) v4) (_ bv0 7)) (_ bv1 1) (_ bv0 1)))) (_ bv0 11) ((_ extract 10 0) (bvlshr (concat (_ bv0 5) (concat (ite (= (_ bv1 1) ((_ extract 0 0) _let_12)) (_ bv1023 10) (_ bv0 10)) _let_12)) ((_ zero_extend 12) ((_ extract 3 0) v4))))) (concat (ite _let_13 (_ bv1023 10) (_ bv0 10)) _let_0)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))) (let ((_let_37 ((_ extract 3 3) _let_34))) (let ((_let_38 ((_ extract 3 3) _let_36))) (let ((_let_39 (ite (bvult ((_ extract 2 0) _let_34) ((_ extract 2 0) _let_36)) (_ bv1 1) (_ bv0 1)))) (let ((_let_40 (bvnot _let_38))) (let ((_let_41 (concat (_ bv0 3) (ite (= (_ bv1 1) (bvand (bvnot (bvand ((_ extract 3 3) _let_18) (bvnot ((_ extract 3 3) _let_18)))) (bvand (bvnot (bvand (bvand (bvnot ((_ extract 3 3) _let_18)) (bvnot ((_ extract 3 3) _let_18))) _let_35)) (bvnot (bvand (bvand ((_ extract 3 3) _let_18) ((_ extract 3 3) _let_18)) _let_35))))) (_ bv1 1) (_ bv0 1))))) (let ((_let_42 ((_ extract 3 3) _let_14))) (let ((_let_43 ((_ extract 3 3) _let_41))) (let ((_let_44 (ite (bvult ((_ extract 2 0) _let_14) ((_ extract 2 0) _let_41)) (_ bv1 1) (_ bv0 1)))) (let ((_let_45 (bvnot _let_43))) (let ((_let_46 (ite (= (ite (= (_ bv1 1) (bvand (bvnot (bvand _let_42 _let_45)) (bvand (bvnot (bvand (bvand (bvnot _let_42) _let_45) _let_44)) (bvnot (bvand (bvand _let_42 _let_43) _let_44))))) (_ bv1 1) (_ bv0 1)) (_ bv0 1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_47 (ite (= (ite (= (_ bv1 1) (bvand (ite (= (_ bv1 1) (bvand (bvnot (bvand _let_24 _let_27)) (bvand (bvnot (bvand (bvand (bvnot _let_24) _let_27) _let_26)) (bvnot (bvand (bvand _let_24 _let_25) _let_26))))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (= (_ bv1 1) (ite (= v3 v2) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (_ bv1 1) (_ bv0 1)))) (let ((_let_48 (bvand (bvnot (bvand (bvnot (bvand (bvnot _let_46) (bvnot _let_47))) (bvnot (bvand _let_46 _let_47)))) (bvand (bvnot (ite (= (ite (= (_ bv1 1) (bvand (ite (= (_ bv1 1) (bvnot (bvand (bvnot (bvand _let_29 _let_32)) (bvand (bvnot (bvand (bvand (bvnot _let_29) _let_32) _let_31)) (bvnot (bvand (bvand _let_29 _let_30) _let_31)))))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (= (_ bv1 1) (bvnot (ite (bvult (concat (ite _let_13 (_ bv7 3) (_ bv0 3)) _let_0) _let_6) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= (ite (= (_ bv1 1) (bvnot (ite (bvult (ite (= (_ bv1 1) (ite (bvult v4 (concat (_ bv0 10) (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv1 1) (bvand (bvnot (bvand _let_2 _let_5)) (bvand (bvnot (bvand (bvand (bvnot _let_2) _let_5) _let_4)) (bvnot (bvand (bvand _let_2 _let_3) _let_4))))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (_ bv0 1)) (_ bv1 1) (_ bv0 1))))))) (let ((_let_49 (bvand (bvnot (ite (= (ite (= (_ bv1 1) (bvnot (bvand (ite (= (_ bv1 1) (ite (bvult (concat (_ bv0 9) _let_17) (_ bv479 10)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) _let_0))) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (_ bv1 1) (_ bv0 1))) (bvnot (bvand (bvnot (ite (= (ite (= (_ bv1 1) (bvnot (bvand (bvnot (bvand _let_37 _let_40)) (bvand (bvnot (bvand (bvand (bvnot _let_37) _let_40) _let_39)) (bvnot (bvand (bvand _let_37 _let_38) _let_39)))))) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (_ bv1 1) (_ bv0 1))) (bvnot (ite (= (ite (= (_ bv1 1) (bvnot (ite (bvult (ite (= (_ bv1 1) (ite (bvult (concat (ite (= (_ bv1 1) _let_9) (_ bv511 9) (_ bv0 9)) (_ bv2 4)) v0) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv1 1) (bvnot (bvand (bvnot (bvand _let_9 _let_22)) (bvand (bvnot (bvand (bvand _let_11 _let_22) _let_21)) (bvnot (bvand (bvand _let_9 _let_20) _let_21)))))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1)) (_ bv0 1)) (_ bv1 1) (_ bv0 1)))))))) (not (= (bvnot (bvand (bvnot (bvand (bvnot _let_49) _let_48)) (bvnot (bvand _let_49 (bvnot _let_48))))) (_ bv0 1))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)