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, check last year's SMT-COMP results in this division: http://www.smtexec.org/exec/divisionResults.php?jobs=856&division=QF_ABV Hope this helps, Cristian On 01/24/2012 07:20 AM, Daniel Wainwright 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 constraints > we're looking at. > > I can see how STP is integrated in, but the problem I've hit is that > KLEE uses the array type in STP, which I don't believe Yices has an > equivalent of. So my question is, what is the simplest way of > converting the constraints KLEE generates into a form Yices can > understand? I am guessing this may have been considered before as it > is listed as a proposed project on the KLEE website. > > If anyone is aware of other constraint solvers that may be more > closely matched to the form of constraints KLEE expects, or knows of > work that has been done comparing constraint solvers this way, that > would also be helpful. > > Thanks for you help, > Daniel > _______________________________________________ > klee-dev mailing > list klee-dev@keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
