Couple of other articles about Z3 which may be also interesting: http://yurichev.com/writings/z3_rockey.pdf http://blog.yurichev.com/node/86