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/
8 stars 3 forks source link

added subcommand to track statistics of a z3 log file #53

Open Gopiandcode opened 1 month ago

Gopiandcode commented 1 month ago

Hihi yall, I've been trying to debug how different encodings of verification conditions affect how long Z3 takes to dispatch goals and such, have built an additional submodule onto the smt-log parser to dump some summary statistics that might shed some information into what's going on inside Z3.

opening a PR to discuss.

Do yall know of any other stats that might be helpful in this regard?

(also hopefully this time edits by maintainers will work :) image )