I thought people might be interested in knowing about a report sponsored by the London Mathematical Society that I wrote with Daniel Kroening and Tom Melham. It's aim is to explain SMT at a high level to a general audience. Follow the link for more. http://cs.nyu.edu/~barrett/pubs/BKM14-abstract.html Clark Barrett