Open yav opened 5 days ago
This is with version 4.13.0.
The output of get-model produces terms like these:
get-model
(_ as-array f)
where f is a function declaration.
f
When trying to parse this, z3 gives the error:
z3
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.
as-array
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.
This is with version 4.13.0.
The output of
get-modelproduces terms like these:where
fis a function declaration.When trying to parse this,
z3gives the error:Things seem to work if the
as-arrayannotation is omitted, andfis 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-modelis something thatz3can consume.