On 21 Mar 2016 11:19 a.m., "Dan Liew" <[email protected]> wrote: > > > On 21 Mar 2016 10:33 a.m., "Azizul Hakim" <[email protected]> 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
Sorry phone autocorrected incorrectly. It should say However I don't know when S2E forked from KLEE so I don't know if S2E has this capability.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
