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