The 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 dece

The 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