(declare-fun a () (Array (
;