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!
Although SAT is indeed NP-complete, modern solvers are ridiculously fast for the kinds of SAT queries that appear in scenarios like hardware model checking and verification. It's not uncommon for queries with millions of variables and clauses to be solved in a matter of seconds. There are some algorithmic tricks combined with clever data structures and search space exploration heuristics that make this possible.
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.
SAT is NP-complete, but there are certain properties that allow theorem provers to show that a particular instance is overconstrained (and therefore unsatisfiable), or underconstrained (and many solutions exist). It's at a particular point, so-called phase transitions, where one finds the very hard instances. As an example, when characterizing 3-SAT instances by grouping by their ratio of clauses to variables, the very hard instances are grouped around a value of ~4.3.
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