Long day at work, didn't see the thread that grew out of this comment. What do I use Z3 for? Right now, I'm implementing a web browser in Z3 so that Z3 can solve CSS layout queries. Like, "write me a CSS file given this website mockup". But honestly, it's just damn fun to play with, and especially for solving small logic puzzles.

For example, a friend and I were playing a board game where each player had hit points, which they represented with two types of cards: type A had "5" on one side and "1" on the other, and type B had a "20" on one side and a "10" on the other. You'd represent your current hitpoints by displaying some number of these cards (out of 6 of the first type and 3 of the second type) face up, and adding up the totals. So, I wanted to find out: what's the smallest hit point value that I can't represent with some combination of cards? The traditional mathematical approach would be generating functions, but that would require at least pencil and paper. With Z3, I execute:

   (declare-const a1 Int)
   (declare-const a2 Int)
   (declare-const a3 Int)
   (declare-const a4 Int)
   (declare-const a5 Int)
   (declare-const a6 Int)

   (declare-const b1 Int)
   (declare-const b2 Int)
   (declare-const b3 Int)

   (assert (or (= a1 0) (= a1 1) (= a1 5)))
   (assert (or (= a2 0) (= a2 1) (= a2 5)))
   (assert (or (= a3 0) (= a3 1) (= a3 5)))
   (assert (or (= a4 0) (= a4 1) (= a4 5)))
   (assert (or (= a5 0) (= a5 1) (= a5 5)))
   (assert (or (= a6 0) (= a6 1) (= a6 5)))

   (assert (or (= b1 0) (= b1 10) (= b1 20)))
   (assert (or (= b2 0) (= b2 10) (= b2 20)))
   (assert (or (= b3 0) (= b3 10) (= b3 20)))

   (assert (= (+ a1 a2 a3 a4 a5 a6 b1 b2 b3) i))
   (check-sat)))))))

If you run this for different values of i (using push and pop if you're clever; I just called Z3 100 times), you can get a "sat" or "unsat" which tells you whether a particular total is reachable.