[richdougherty]

Z3 has a core engine optimised to solve certain types of problems. To use Z3 for higher-level problems, such as program verification, you first translate your higher-level problems into problems that Z3 understands. Z3 might not be suitable for all problems, but it is meant to be highly optimised for the problems that it can handle.

http://research.microsoft.com/en-us/um/redmond/projects/z3/z... http://research.microsoft.com/en-us/um/people/leonardo/files... http://research.microsoft.com/en-us/events/z3dtu/dtu-jan4-z3...