Boolector http://fmv.jku.at/boolector/ の2.0.0がリリースされていた。https://groups.google.com/d/msg/boolector/gpCTYeny5dc/A4OJB4dxPEoJ

uninterpreted function への対応なんかも加わっているのね。Boolectorはビットベクタと配列の理論に特化したSMTソルバで、Nelson-Oppen theory combination などの汎用的な theory combination のオーバーヘッドを嫌っていたと思うが、何か特別な方法を使ったのかな？