Z3-str: A Z3-based String Solver for Web Application Analysis http://portal.acm.org/citation.cfm?id=2491411.2491456 文字列の理論のソルバとしても面白いけれど、Z3がソース公開する前に作っていたようで、プラグインの仕組みでこんな感じで拡張できるのか、というのも面白かった。 コア(DPLLとEUF)の機能をうまく使ってやることで、比較的省力化されてる感じ。