(declare-fun f () (epected_underscore_or_Array