(set-logic QF_BV)
(set-info :status sat)
(declare-const v0 (_ BitVec 1))
(declare-const v1 (_ BitVec 1))
(declare-const v2 (_ BitVec 1))
(declare-const v3 (_ BitVec 13))
(declare-const v4 (_ BitVec 9))
(declare-const v5 (_ BitVec 5))
(declare-const v6 (_ BitVec 4))
(declare-const v7 (_ BitVec 1))
(declare-const v8 (_ BitVec 4))
(declare-const v9 (_ BitVec 1))
(declare-const v10 (_ BitVec 5))
(assert (= #b1 (bvand (bvnot (bvand (ite (= (ite (= (bvand (bvnot v0) (bvand (bvnot (bvand v1 v2)) (bvnot (bvand (bvand ((_ extract 12 12) (concat (bvnot (_ bv0 12)) (ite (= (ite (bvult (bvnot (_ bv0 1)) #b0) #b1 #b0) #b1) (bvnot (_ bv0 1)) #b0))) ((_ extract 12 12) (bvnot (ite (= (bvnot (ite (= ((_ extract 12 4) v3) v4) #b1 #b0)) #b1) (bvnot (_ bv0 13)) ((_ extract 12 0) (ite (= ((_ extract 15 15) (concat (ite (= ((_ extract 12 12) (concat #b00000000 v5)) #b1) #b111 (_ bv0 3)) (concat #b00000000 v5))) #b1) (bvnot (bvlshr (bvnot (concat (ite (= ((_ extract 12 12) (concat #b00000000 v5)) #b1) #b111 (_ bv0 3)) (concat #b00000000 v5))) ((_ zero_extend 12) v6))) (_ bv0 16))))))) v2)))) #b1) (bvnot (_ bv0 1)) #b0) (bvnot (_ bv0 1))) #b1 #b0) (bvnot (ite (= (ite (= (bvand (bvnot (bvand ((_ extract 4 4) (bvadd (bvnot (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001)) #b00001)) (bvnot ((_ extract 4 4) (bvudiv (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001) (concat (_ bv0 4) (bvnot (_ bv0 1)))))))) (bvand (bvnot (bvand (bvand (bvnot ((_ extract 4 4) (bvadd (bvnot (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001)) #b00001))) (bvnot ((_ extract 4 4) (bvudiv (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001) (concat (_ bv0 4) (bvnot (_ bv0 1))))))) (ite (bvult ((_ extract 3 0) (bvadd (bvnot (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001)) #b00001)) ((_ extract 3 0) (bvudiv (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001) (concat (_ bv0 4) (bvnot (_ bv0 1)))))) #b1 #b0))) (bvnot (bvand (bvand ((_ extract 4 4) (bvadd (bvnot (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001)) #b00001)) ((_ extract 4 4) (bvudiv (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001) (concat (_ bv0 4) (bvnot (_ bv0 1)))))) (ite (bvult ((_ extract 3 0) (bvadd (bvnot (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001)) #b00001)) ((_ extract 3 0) (bvudiv (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001) (concat (_ bv0 4) (bvnot (_ bv0 1)))))) #b1 #b0))))) #b1) (bvnot (_ bv0 1)) #b0) (bvnot (_ bv0 1))) #b1 #b0)))) (bvand (ite (= (ite (= (bvnot (bvand v7 (ite (bvult v8 v8) #b1 #b0))) #b1) (bvnot (_ bv0 1)) #b0) (bvnot (_ bv0 1))) #b1 #b0) (ite (= (concat (_ bv0 4) (ite (= (bvand ((_ extract 4 4) (bvadd (bvnot (bvand (bvnot (ite (= v9 #b1) (bvadd (bvnot (bvurem v10 v10)) #b00001) (bvurem v10 v10))) (bvnot (concat (_ bv0 4) (bvnot (_ bv0 1)))))) (bvadd (bvnot (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b00001))) (bvnot ((_ extract 4 4) (_ bv0 5)))) #b1) (bvnot (_ bv0 1)) #b0)) (concat ((_ extract 3 0) v5) ((_ extract 4 4) v5))) #b1 #b0)))))
(check-sat)