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 [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
