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 <[email protected]> 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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
