Hi all, We have recently developed a version of KLEE which supports Z3, Boolector and STP. As Dan mentioned, we have used the metaSMT framework (http://www.informatik.uni-bremen.de/agra/eng/metasmt.php), which provides a unified API for using a number of SMT (and SAT) solvers through their own API's. You can find some information about the project here:
http://srg.doc.ic.ac.uk/projects/klee-multisolver/ We plan to start to slowly integrate the changes into mainline KLEE, but if you'd like more information in the mean time, please drop me an email. Best regards, Hristina > 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] > <mailto:[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
