[klee-dev] How to Interpret Klee Path Predicate

[Dan Liew]

On 4 April 2016 at 17:55, Azizul Hakim <azizulfahim2002 at gmail.com> wrote:
> Thanks Dan.   I can also print the constraints in the format below. Do you
> happen to have any idea where I can get a documentation of this format?
>
>
>
> (query [(Eq false
>             (Eq (w32 0x0)
>                 (And w32 (Add w32 (w32 0xfffffffe)
>                                   (ZExt w32 (Read w8 0x0 v0_str_0)))
>                          (w32 0xff))))]
>        false)
>
>
>
> Thanks for your time.
>

That is the [kQuery format](https://klee.github.io/docs/kquery/) which
is specific to KLEE. One thing you could try doing is porting the
ExprSMTLIBPrinter to your fork of KLEE, it shouldn't be too difficult.