On 07/06/2011 23:40, Vijay Ganesh wrote: > On Tue, Jun 7, 2011 at 5:38 PM, Cristian Cadar > <c.cadar at imperial.ac.uk <mailto:c.cadar at imperial.ac.uk>> wrote: > > On 07/06/2011 12:12, Russell Wallace wrote: >> 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. > > STP was initially developed in conjunction with KLEE's precursor, > EXE, and has many optimizations that are useful for symbolic > execution (see > http://www.doc.ic.ac.uk/~cristic/papers/exe-ccs-06.pdf > <http://www.doc.ic.ac.uk/%7Ecristic/papers/exe-ccs-06.pdf> for > details). > > > To this I would add that STP has been continuously improved over the > years, and it performs consistently better than other solvers for > bit-vectors and arrays (It won the SMTCOMP 2010 for bit-vectors).
BTW, Peter Collingbourne has recently added a --with-stp option that can be used to select an arbitrary version of STP (http://llvm.org/viewvc/llvm-project?view=rev&revision=108347). We have indeed observed a significant performance improvement with newer versions of STP on certain benchmarks. Best, Cristian
