(declare-fun a () (Array (_ BitVec 
2147483648