search

viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
Apache License 2.0
16 stars 3 forks source link

Compose Expressions? #59

Open Philipp15b opened 5 months ago

Philipp15b commented 5 months ago

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 (https://github.com/Z3Prover/z3/issues/4571). Caesar is using Z3 4.12.1.0, which should include the fix. But I still see this issue.

Thanks a lot!

JonasAlaif commented 1 week ago

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!