(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) (assert (=> a true)