[klee-dev] KLEE-MultiSolver now available
Cristian Cadar
c.cadar at imperial.ac.uk
Wed Oct 23 19:04:45 BST 2013
Thanks to Hristina Palikareva, our multi-solver extension to KLEE is now
available as part of mainline KLEE. The KLEE-MultiSolver extension is
based on the metaSMT framework and is described in detail in our CAV'13
paper (see
http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html).
While STP remains the default solver in KLEE, now you can also switch to
Boolector or Z3 with a simple command-line flag (e.g.,
--use-metasmt=z3). Adding additional metaSMT-compatible solvers should
be quite easy.
To enable support for multiple solvers, you need to follow the
instructions at http://srg.doc.ic.ac.uk/projects/klee-multisolver/.
Please let us know if you run into any issues.
Cristian
More information about the klee-dev
mailing list