[klee-dev] How to Interpret Klee Path Predicate

[Dan Liew]

On 21 Mar 2016 10:33 a.m., "Azizul Hakim" <azizulfahim2002 at gmail.com> wrote:
>
> How do we interpret the path predicates generated by KLEE. I've the
following path predicates generated by S2E tool which uses KLEE. This
predicate is generated from one branch of an IF-ELSE statement.
>

IIRC you're looking at STP's internal format which I think is based on
CVC's internal format

http://cvc4.cs.nyu.edu/wiki/CVC4%27s_native_language

Mainline KLEE supports emitting constraints in the SMT-LIBv2 format which
is more widely used and documented. However I don't know when S2E forked
from KLEE so I find know if S2E has this capability

HTH,
Dan
-------------- next part --------------
HTML attachment scrubbed and removed