[klee-dev] z3 for klee

[Daniel Liew]

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> 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.
>
-------------- next part --------------
HTML attachment scrubbed and removed