(set-logic QF_ABV)
(declare-fun a () (Array (_ BitVec 64) (_ BitVec 1)))
(assert a)