I notice Klee chose STP for its SMT solver. I'm curious as to the reason for this choice, and whether it would still be considered the best today? The reason I ask is that I'm planning some experiments in symbolic execution, and currently the list of potentially suitable off-the-shelf solvers seems to be Beaver, Boolector, CVC3, OpenSMT, Sateen, Sonolar, STP, Verit; which is a long list. I'm wondering how to narrow it down.
In particular, I notice some of the systems advertise the ability to perform bit vector arithmetic, whereas others only advertise general integer arithmetic. Is that a critical difference, or will a general integer system more or less suffice? (I asked a similar question at http://stackoverflow.com/questions/6263962/smt-solvers-for-bit-vector-arithmetic but no replies yet - obviously this is a somewhat specialized topic.)
