Z3 is about "satisfiability modulo theories", which basically means a SAT solver with smart extensions for things like floating point arithmetic that would otherwise die under a naive encoding. It's used for program verification, and in my group, program synthesis. OR tools like Google's choke on such problems that require reasoning about logic, recursive functions, etc.

For an example of a program verifier using Z3, Pex is amazing: pex4fun.com . It does 'whitebox' fuzzing (program analysis + SMT) to find inputs that break your assert statements and open-ended unit tests.

For an example of a program synthesizer, I spent the past few days writing a regular expression / sed script generator that infers the code from input/output pairs: http://lmeyerov.blogspot.com/2013/09/sneak-peek-for-my-stran... . Underneath, it calls into a SAT solver (it goes through Rosette[1], which plugs in its own solver or Z3).

[1] http://splashcon.org/2013/program/onward-research-papers/909...