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!

[JonasAlaif]

Hey! Did you manage to fix this/find a version of z3 that worked in the end? If not could you please attach smt2/log files and let me know which versions of z3 you've tried so I can take a look at it. Thanks!

[ole-thoeb]

It really seems to be related to pretty-printing. This problem only occurs if the SMT-lib code is printed before verification. So apparently Z3Prover/z3#4571 is not fixed (or regressed) in 4.12.1.0.
For now, we have a simple workaround by not printing the SMT-lib when tracing z3.