[ufo]

It might be better to see Ze and other SMT solvers as souped up SAT solvers instead of comparing them to general theorem provers.

The neat thing about Z3 is that it has efficient solvers for the more specific subproblems (linear programming, bit vectors, etc) that you can't have if you state everything using "general" constraint programming. At the same time, Z3 lets you work at a higher level of abstraction - for example, you can reason about bit verctors or arithmetic directly instead of having to encode it with boolean formulas.