DANGER! DANGER! DANGER!
This can potentially kill us:
Looking at a live Z3 Bool "(= x y)", one cannot tell whether it is an Iff between two formulae in the metalanguage (something like p⇔q), or an equality predicate between two terms (a=b) which just happen to be terms of Book sort.
I can not think of a way to properly fix this confusion between object- and metalanguage if we are to stick with live Z3 ASTs.
DANGER! DANGER! DANGER! This can potentially kill us: Looking at a live Z3 Bool "(= x y)", one cannot tell whether it is an Iff between two formulae in the metalanguage (something like p⇔q), or an equality predicate between two terms (a=b) which just happen to be terms of Book sort.
I can not think of a way to properly fix this confusion between object- and metalanguage if we are to stick with live Z3 ASTs.