(set-logic QF_BV)
(set-info :status sat)
(declare-const v0 (_ BitVec 4))
(declare-const v1 (_ BitVec 4))
(declare-const v2 (_ BitVec 4))
(declare-const v3 (_ BitVec 2))
(declare-const v4 (_ BitVec 2))
(declare-const v5 (_ BitVec 1))
(declare-const v6 (_ BitVec 1))
(declare-const v7 (_ BitVec 1))
(assert (= #b1 (bvand (bvand (bvand (bvand (ite (= v3 ((_ extract 3 2) v1)) #b1 #b0) (ite (= #b1 v5) #b1 #b0)) (bvand (ite (= v4 ((_ extract 3 2) v2)) #b1 #b0) (ite (= #b1 v6) #b1 #b0))) (bvand (bvand (ite (= #b1 v7) #b1 #b0) (ite (= v0 (bvmul v1 v2)) #b1 #b0)) (bvand (bvnot (bvand (bvnot (bvand (bvnot (ite (= v5 #b1) #b1 #b0)) (bvnot (ite (= v3 #b00) #b1 #b0)))) (bvnot (bvand (ite (= v5 #b1) #b1 #b0) (ite (= v3 #b00) #b1 #b0))))) (bvnot (bvand (bvnot (bvand (bvnot (ite (= v6 #b1) #b1 #b0)) (bvnot (ite (= v4 #b00) #b1 #b0)))) (bvnot (bvand (ite (= v6 #b1) #b1 #b0) (ite (= v4 #b00) #b1 #b0)))))))) (bvnot (bvand (bvnot (bvand (bvnot (ite (= v7 #b1) #b1 #b0)) (bvnot (ite (= #b1001 v0) #b1 #b0)))) (bvnot (bvand (ite (= v7 #b1) #b1 #b0) (ite (= #b1001 v0) #b1 #b0))))))))
(check-sat)