Skip to content

[prove] more statistics

Loïc Correnson requested to merge feature/more-stats into master

Output per-prover and per-tactics statistics at then end of proving.

Typical output :

$ why3find prove foo.mlw -P -cvc4 -l
Warning: prover cvc4@1.8 not configured (project)
Theory foo.Bar: ✔ (197)
Cache 205/210
Proofs ✔ (197)
 - unchanged: 195
 - updated: 2
Provers 4.7s (+1.3s), depth: 1
 - alt-ergo@2.5.4       ( 166) ( 28ms - 206ms -  2.9s)
 - z3@4.8.15            (  29) ( 39ms - 306ms - 920ms)
 - cvc5@1.0.9           (   2) ( 2.7s -  3.7s -  4.7s)
 - split_vc             (   1)
Emitted 1 warning
Edited by Loïc Correnson

Merge request reports

Loading