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?
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.
See the result tables in http://arxiv.org/abs/1004.5034 . Pay attention to the "Simplify" column.