[klee-dev] Metasmt using Z3 for getting unsat core

[Thuan Pham]

Hi,
I haven't tried to work with Z3 through metasmt. However, in our previous
work (Hercules: reproducing crashes in real-world application binaries), I
implemented an interface function for S2E (which is built on top of KLEE
and QEMU) to get unsat-core from Z3. What I did is to formulate a SMT
LIB-v2 query, save it to a file and invoke Z3 (as an external process) to
get unsat-core (if the query is unsat). An example of the query is here
http://rise4fun.com/Z3/smtc_core.

If you want to get unsat-core from Z3 directly through metasmt interface, I
think you just need to know the interface between KLEE and metasmt,
formulate your query and send it through the interface.
Hope it helps,
Regards,
Thuan

On Tue, Sep 22, 2015 at 7:58 PM, felicia <felicia at comp.nus.edu.sg> wrote:

> Hi,
>
> I have installed metasmt and use Z3 as a solver. I actually need to
> implement code in KLEE
> where Z3 solver able to produce unsat-core. I am currently still not sure
> how I implement it in KLEE.
> I really appreciate if you can give suggestion about this.
>
> Thank you very much.
> Best Regards,
>
>
> Sent from Samsung Mobile
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed