Hi Heming, KLEE currently has no API for reading back constraints (although you might be able to restructure your equivalence query so that it's directly generated by an assert statement that KLEE can check), but I think you should be able to use STP directly for this.
Best, Cristian On 23/04/10 06:12, Heming Cui wrote: > Dear all, > I have run some experiments to collect two sets of constraints, > each set contains the same number and type of symbolic variables. I am > wondering whether KLEE has some APIs to judge these two sets of > constraints are equavalent (i.e., given the same concrete values for the > symbolic variables, the two sets always produce the same result)? > > -- > Regards, > Heming Cui
