I've used model checkers before, but never SMT solvers. Looks really cool!

Anyway, here's a great post on solving a Project Euler problem using Z3/SMT-lib, which may be inspiring for other novices like myself:

http://blogs.teamb.com/craigstuntz/2014/07/07/38818/