`z3` cannot understand the models it produces

[yav]

This is with version 4.13.0.

The output of get-model produces terms like these:

(_ as-array f)

where f is a function declaration.

When trying to parse this, z3 gives the error:

invalid function declaration reference, named expressions (aka macros) cannot be referenced `f`

Things seem to work if the as-array annotation is omitted, and f is used directly, which seems confusing.

I don't think it matters very much which way things are done, but it would be nice if the result of get-model is something that z3 can consume.