Cristian Cadar
2013-10-23 18:04:45 UTC
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
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