(set-logic QF_BV)
(set-info :status unsat)
(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 (distinct (concat (concat (concat v0 v1) (concat v2 v3)) (concat (concat v4 v5) (concat v6 v7))) (concat (concat (concat (concat (concat (concat (concat v0 v1) v2) v3) v4) v5) v6) v7)) #b1 #b0)))
(check-sat)