4 ms·
Where does the "world's fastest" claim come from, and how was it determined? Z3 is a good SMT prover for some formulas that come from program verification, but
by pascal_cuoq 16y ago
Where does the "world's fastest" claim come from, and how was it determined? Z3 is a good SMT prover for some formulas that come from program verification, but it is neither uniformly better nor faster than other provers, one of which predates it by what, 10 years?
See the result tables in http://arxiv.org/abs/1004.5034 http://arxiv.org/abs/1004.5034 . Pay attention to the "Simplify" column.
- jaen 16y agoThe benchmark for theorem provers is the CADE theorem proving competition [1]. For SMT provers there's SMT-COMP [2]. Z3 last participated in 2008 [3], with decent results, but "world's fastest" seems a bit too generous. [1] http://www.cs.miami.edu/~tptp/CASC/ http://www.cs.miami.edu/~tptp/CASC/ [2] http://www.smtcomp.org/2010/ http://www.smtcomp.org/2010/ [3] http://www.smtexec.org/exec/?jobs=311 http://www.smtexec.org/exec/?jobs=311