Hi, To my knowledge this has already been done twice.
* By myself via SMTLIBv2 files ( see https://github.com/delcypher/klee/tree/smtlib ). Invoking smtlib solvers this way proved to be quite slow. This work allows any smtlibv2 solver that supports the (get-value) command to be used by KLEE. STP itself can be used this way too by using a small wrapper (stpwrap2). Z3 works without a wrapper. * By Hristina Palikareva using the meta-smt API. I'm not sure how much of this work is published so I shall leave her to comment on this. Regards, Dan Liew On 7 Jun 2013 16:09, "K Kylin" <[email protected]> wrote: > Hello, > I'm trying to make z3 into klee instead stp solver. with my mentor's > advice that z3 is more efficient. Maybe some work have been done by any of > you. If someone is doing this work, let me take part in, or if anyone > interest in it let's do it together. > thank you. >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
