(set-logic QF_BV)
(set-info :status sat)
(declare-const v0 (_ BitVec 8))
(declare-const v1 (_ BitVec 8))
(declare-const v2 (_ BitVec 8))
(declare-const v3 (_ BitVec 8))
(declare-const v4 (_ BitVec 8))
(declare-const v5 (_ BitVec 8))
(declare-const v6 (_ BitVec 8))
(declare-const v7 (_ BitVec 8))
(assert (= #b1 (ite (= v3 (bvadd v0 v1)) #b1 #b0)))
(assert (= #b1 (ite (= v1 (bvadd v4 v2)) #b1 #b0)))
(assert (= #b1 (ite (= v2 (bvadd (_ bv7 8) v4)) #b1 #b0)))
(assert (= #b1 (ite (= v4 (bvmul (_ bv2 8) v3)) #b1 #b0)))
(assert (= #b1 (ite (= v6 (bvadd (bvmul (_ bv3 8) v1) v7)) #b1 #b0)))
(assert (= #b1 (ite (= v7 (bvmul (_ bv7 8) v5)) #b1 #b0)))
(check-sat)