(set-logic QF_ABV)
(declare-fun initialMemoryState_0x2ae2bf0 () (Array (_ BitVec 64) (_ BitVec 8)))
(assert
(let ((x1 (_ bv1 8)))
(let ((x2 (_ bv0 32)))
(let ((x3 (_ bv3221225470 64)))
(let ((x4 (_ bv3221225468 64)))
(let ((x5 initialMemoryState_0x2ae2bf0))
(let ((x6 (_ bv3221225468 64)))
(let ((x7 ((_ extract 7 0) x2)))
(let ((x8 (store x5 x6 x7)))
(let ((x9 (_ bv3221225469 64)))
(let ((x10 ((_ extract 15 8) x2)))
(let ((x11 (store x8 x9 x10)))
(let ((x12 (_ bv3221225470 64)))
(let ((x13 ((_ extract 23 16) x2)))
(let ((x14 (store x11 x12 x13)))
(let ((x15 (_ bv3221225471 64)))
(let ((x16 ((_ extract 31 24) x2)))
(let ((x17 (store x14 x15 x16)))
(let ((x18 (store x17 x3 x1)))
(let ((x19 (_ bv3221225468 64)))
(let ((x20 (select x18 x19)))
(let ((x21 (_ bv3221225469 64)))
(let ((x22 (select x18 x21)))
(let ((x23 (_ bv3221225470 64)))
(let ((x24 (select x18 x23)))
(let ((x25 (_ bv3221225471 64)))
(let ((x26 (select x18 x25)))
(let ((x27 (concat x22 x20)))
(let ((x28 (concat x24 x27)))
(let ((x29 (concat x26 x28)))
(let ((dollar_x30 (not (=  x29 x2))))
(let ((dollar_x31 (not dollar_x30)))
dollar_x31
)))))))))))))))))))))))))))))))
)
(check-sat)
(exit)