; benchmark

(set-info :status unknown)

(set-logic QF_AUFBV)

(declare-fun x1 () (_ BitVec 8))

(declare-fun x0 () (_ BitVec 8))

(declare-fun x31 () (_ BitVec 8))

(declare-fun x30 () (_ BitVec 8))

(declare-fun x19 () (_ BitVec 8))

(declare-fun x18 () (_ BitVec 8))

(declare-fun x9 () (_ BitVec 8))

(declare-fun x8 () (_ BitVec 8))

(declare-fun x29 () (_ BitVec 8))

(declare-fun x28 () (_ BitVec 8))

(declare-fun x27 () (_ BitVec 8))

(declare-fun x26 () (_ BitVec 8))

(declare-fun x25 () (_ BitVec 8))

(declare-fun x24 () (_ BitVec 8))

(declare-fun x17 () (_ BitVec 8))

(declare-fun x16 () (_ BitVec 8))

(declare-fun x23 () (_ BitVec 8))

(declare-fun x22 () (_ BitVec 8))

(declare-fun x21 () (_ BitVec 8))

(declare-fun x20 () (_ BitVec 8))

(declare-fun x15 () (_ BitVec 8))

(declare-fun x14 () (_ BitVec 8))

(declare-fun x13 () (_ BitVec 8))

(declare-fun x12 () (_ BitVec 8))

(declare-fun x7 () (_ BitVec 8))

(declare-fun x6 () (_ BitVec 8))

(declare-fun x11 () (_ BitVec 8))

(declare-fun x10 () (_ BitVec 8))

(declare-fun x5 () (_ BitVec 8))

(declare-fun x4 () (_ BitVec 8))

(declare-fun x3 () (_ BitVec 8))

(declare-fun x2 () (_ BitVec 8))

(assert

(let ((?x206 (bvand (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)) (_ bv3840 16))))

(let ((?x209 (bvxor (bvadd ?x206 (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1))) (_ bv40852 16))))

(let (($x210 (= ?x209 (_ bv0 16))))

(let ((?x82 (bvor (bvshl ((_ zero_extend 8) x8) (_ bv8 16)) ((_ zero_extend 8) x9))))

(let ((?x200 (bvadd (bvor (bvshl ((_ zero_extend 8) x28) (_ bv8 16)) ((_ zero_extend 8) x29)) ?x82)))

(let ((?x201 (bvadd ?x200 (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)))))

(let (($x204 (= (bvxor ?x201 (_ bv61624 16)) (_ bv0 16))))

(let ((?x190 (bvxor (bvor (bvshl ((_ zero_extend 8) x26) (_ bv8 16)) ((_ zero_extend 8) x27)) (_ bv34364 16))))

(let (($x195 (= (bvxor (bvadd ?x190 (_ bv4660 16)) (_ bv37139 16)) (_ bv0 16))))

(let ((?x183 (bvxor (bvor (bvshl ((_ zero_extend 8) x24) (_ bv8 16)) ((_ zero_extend 8) x25)) (_ bv2139 16))))

(let (($x184 (= ?x183 (_ bv0 16))))

(let ((?x174 (bvadd (bvor (bvshl ((_ zero_extend 8) x22) (_ bv8 16)) ((_ zero_extend 8) x23)) (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)))))

(let (($x177 (= (bvxor ?x174 (_ bv37640 16)) (_ bv0 16))))

(let ((?x165 (bvxor (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)) (_ bv2642 16))))

(let ((?x163 (bvadd (bvor (bvshl ((_ zero_extend 8) x18) (_ bv8 16)) ((_ zero_extend 8) x19)) (_ bv16388 16))))

(let (($x169 (= (bvxor (bvadd ?x163 ?x165) (_ bv25202 16)) (_ bv0 16))))

(let ((?x154 (bvxor (bvor (bvshl ((_ zero_extend 8) x16) (_ bv8 16)) ((_ zero_extend 8) x17)) (_ bv34563 16))))

(let (($x157 (= (bvxor ?x154 (_ bv12598 16)) (_ bv0 16))))

(let ((?x145 (bvadd (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) (_ bv4626 16))))

(let (($x148 (= (bvxor ?x145 (_ bv5783 16)) (_ bv0 16))))

(let ((?x107 (bvor (bvshl ((_ zero_extend 8) x12) (_ bv8 16)) ((_ zero_extend 8) x13))))

(let (($x143 (= (bvxor (bvor (bvadd ?x107 (_ bv21554 16)) (_ bv12296 16)) (_ bv15224 16)) (_ bv0 16))))

(let ((?x78 (bvor (bvshl ((_ zero_extend 8) x6) (_ bv8 16)) ((_ zero_extend 8) x7))))

(let ((?x132 (bvadd (bvor (bvshl ((_ zero_extend 8) x10) (_ bv8 16)) ((_ zero_extend 8) x11)) ?x78)))

(let (($x136 (= (bvxor (bvadd ?x132 ?x107) (_ bv57128 16)) (_ bv0 16))))

(let ((?x124 (bvmul ?x82 (bvor (bvshl ((_ zero_extend 8) x30) (_ bv8 16)) ((_ zero_extend 8) x31)))))

(let (($x127 (= (bvxor ?x124 (_ bv31720 16)) (_ bv0 16))))

(let (($x119 (= (bvxor (bvadd (bvxor ?x78 (_ bv50651 16)) (_ bv5290 16)) (_ bv20493 16)) (_ bv0 16))))

(let ((?x108 (bvmul (bvor (bvshl ((_ zero_extend 8) x14) (_ bv8 16)) ((_ zero_extend 8) x15)) ?x107)))

(let ((?x109 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x4) (_ bv8 16)) ((_ zero_extend 8) x5)) (_ bv51167 16)) ?x108)))

(let (($x112 (= (bvxor ?x109 (_ bv60272 16)) (_ bv0 16))))

(let ((?x90 (bvmul (bvmul ?x78 ?x82) (bvxor (bvor (bvshl ((_ zero_extend 8) x2) (_ bv8 16)) ((_ zero_extend 8) x3)) (_ bv4063 16)))))

(let (($x93 (= (bvxor ?x90 (_ bv15832 16)) (_ bv0 16))))

(let ((?x50 (bvadd (bvxor (bvor (bvshl ((_ zero_extend 8) x0) (_ bv8 16)) ((_ zero_extend 8) x1)) (_ bv18742 16)) (bvor (bvshl ((_ zero_extend 8) x20) (_ bv8 16)) ((_ zero_extend 8) x21)))))

(let (($x54 (= (bvxor ?x50 (_ bv31989 16)) (_ bv0 16))))

(and $x54 $x93 $x112 $x119 $x127 $x136 $x143 $x148 $x157 $x169 $x177 $x184 $x195 $x204 $x210)))))))))))))))))))))))))))))))))))))

(check-sat)