Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
See "SMT Solvers: Disruptive Innovation in Theorem Proving", Rushby, 2007.
> SAT solving is the quintessential NP-complete problem. But now amazingly fast in practice (most of the time)
> SMT ... generalizes SAT solving by adding the ability to handle arithmetic and other decidable theories
btw, if you're curious about the workings of a modern SAT solver, the first few sections of this paper: http://www.georg.weissenbacher.name/papers/mod12.pdf should make interesting and hopefully accessible reading.
Unfortunately, I don't know enough about the internals of Z3 to know what specifically makes it the fastest SMT solver. But I also don't think it's too far wrong to say that SMT solvers like Z3 are fast because the underlying SAT solver they use is very fast.