Compose Expressions?

[Philipp15b]

Hello everyone!

This project looks amazing. However, I loaded a simple trace from the Caesar verifier and got a bunch of objects that look like internal formatting expressions everywhere. For example, there's stuff like this:

Body: ∀ exponent!9
: Int, base!8
: Real. {string} compose(string, string) ∨ ¬compose(string, string) ∨ indent(compose(string, compose(indent(compose(string, string)), indent(compose(string, string, compose(string, string), string))), compose(string, string, string, string), string))

These function applications do seem to show up in the original z3 trace as well, so it's probably not an issue with the axiom profiler. But maybe you have some advice where this might come from?

Edit: It looks like there was a previous issue of Z3 where this happened (Z3Prover/z3#4571). Caesar is using Z3 4.12.1.0, which should include the fix. But I still see this issue.

Thanks a lot!