[klee-dev] z3 for klee

[Hristina Palikareva]

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" <kylinsmail at gmail.com
> <mailto:kylinsmail at gmail.com>> 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.
>