(declare-fun a () (Array (_ BitVector ;<- Typo: should be BitVec