Runs online · Tutorial

A tool for visualising, analysing and understanding quantifier instantiations made via E-matching in a run of an SMT solver (at present, only Z3 has been modified to provide the necessary log files). The tool takes a log file (which can be generated by Z3 by passing additional command-line options; see below) and presents information visually, primarily using a graph representation of the quantifier instantiations made and their causal connections. This graph can be filtered and explored in a variety of ways, and detailed explanations of individual quantifier instantiations are assembled and displayed. A range of customisations are available for aiding the presentation and understanding of this information, including explanations of equalities used to justify a quantifier instantiation.

This tool supersedes the Axiom Profiler. S_^MTS_^COPE is more stable, ~10x faster and is better a debugging z3 performance issues.

More details of the tool's features can be found in the README of the old tool.

Obtaining a z3 trace

NOTE: S_^MTS_^COPE requires at least version 4.8.5 of z3.

Run Z3 with two extra command-line options:

z3 trace=true proof=true ./input.smt2

This will produce a trace file called ./z3.log. If you want to specify the target filename, you can pass a third option:

z3 trace=true proof=true trace-file-name=foo.log ./input.smt2

NOTE: if this takes too long, it is possible to run S_^MTS_^COPE with a prefix of a valid trace file - you could potentially kill the z3 process and obtain the corresponding partial trace. Some users (especially on Windows) have reported that killing z3 can cause a lot of the file contents to disappear; if you observe this problem, it's recommended to copy the trace file before killing the process.

Similarly, if you have a trace file which takes too long to load into S_^MTS_^COPE, hitting Cancel will cause the tool to work with the portion loaded so far.

To correctly parse the trace file, we impose a few restrictions on the smt2 file given to z3.

Obtaining a trace from various verification tools that use z3 (feel free to add more)

Boogie

Boogie can forward flags to z3 with proverOpt:O:.... For example:

boogie /vcsCores:1 /proverOpt:O:trace=true /proverOpt:O:proof=true ./file.bpl

Boogie can also dump the .smt2 file it gives to z3. For example:

boogie /proverLog:query-@[email protected] ./file.bpl

Viper (silicon)

Silicon can dump the .smt2 file it gives to z3. For example:

silicon --numberOfParallelVerifiers 1 --proverLogFile query ./file.vpr

Then use the z3 commands from above to generate the trace file from the resulting .smt2 file.

Silicon can also forward flags to z3 with --z3Args, but when verifying multiple methods/functions the traces for each will be overwritten. For example:

silicon --numberOfParallelVerifiers 1 --z3Args "trace=true proof=true" ./file.vpr

If it complains about an unrecognized argument, try escaping the double-quotes. E.g.:

# Unix-like systems
silicon --numberOfParallelVerifiers 1 --z3Args '"trace=true proof=true"' ./file.vpr

# Windows
silicon --numberOfParallelVerifiers 1 --z3Args """trace=true proof=true""" ./file.vpr

Viper (carbon)

Carbon can forward flags to Boogie with --boogieOpt, then use the same flags as listed there. For example:

carbon --boogieOpt "/vcsCores:1 /proverOpt:O:trace=true /proverOpt:O:proof=true" ./file.vpr

Carbon can also dump the .bpl file it gives to Boogie. For example:

carbon --print ./file.bpl ./file.vpr

Dafny

See these instructions in Dafny's wiki: Investigating slow verification performance.

Dafny does not seem to support getting the trace file with the new configuration options, therefore we need to use the old mode. In the old mode flags are directly forwarded to Boogie. For example:

dafny /compile:0 /vcsCores:1 /proverOpt:O:trace=true /proverOpt:O:proof=true ./file.dfy

This can be used to get the .smt2 file (as above, using /proverLog:query-@[email protected]). Dafny can also dump the .bpl file it gives to Boogie. For example:

dafny /compile:0 /print:file.bpl ./file.dfy

FStar

See these instructions in FStar's wiki: Profiling Z3 queries.

Using the --log_queries flag should dump the .smt2 file it gives to z3.

VerCors

VerCors can forward flags to the silicon backend with --backend-option, then use the same flags as listed there. For example:

vercors ./file.pvl --backend-option --numberOfParallelVerifiers=1 --backend-option --z3Args="trace=true proof=true"