[klee-dev] Add new solver like dreal to backend of klee

Dan Liew dan at su-root.co.uk
Tue Jan 10 19:41:09 GMT 2017


On 10 January 2017 at 18:04, Cx Qingyang <qingyangcx2015 at gmail.com> wrote:
> Hi,i want to add some solver like dreal to the backend of klee,could you
> give some advise?

A Z3 solver backend was added fairly recently. You should take a look
at that as an example of how to do it.

Here's the PR that it was introduced

https://github.com/klee/klee/pull/337

Note that the Z3 code has changed a little bit since this was
committed so you should look at the master branch to see how things
are done currently.

HTH,
Dan.



More information about the klee-dev mailing list