On Tue, Jan 24, 2012 at 8:20 AM, Daniel Wainwright
daniel.j.wainwri...@oracle.com wrote:
Hi,
I would like to try integrating other constraint solvers into KLEE and
Kleaver, probably Yices and maybe some others, to help make an evaluation of
how the solvers perform on the type of path
Hi Daniel,
KLEE requires a constraint solver with support for the theory of
bitvectors and arrays of bitvectors, i.e. QF_ABV in SMT-LIB:
http://goedel.cs.uiowa.edu/smtlib/logics/QF_ABV.smt2
I am not sure whether Yices implements this theory or not, but several
other solvers do. For example,
Hi,
I would like to try integrating other constraint solvers into KLEE and Kleaver,
probably Yices and maybe some others, to help make an evaluation of how the
solvers perform on the type of path constraints we're looking at.
I can see how STP is integrated in, but the problem I've hit is that
