Hi Heming, We don't have a tool for this, but it is easy to write; all you need to do is take the two kquery files, and then query STP to see if the conjunctions of each constraint set is equivalent.
- Daniel On Apr 22, 2010, at 22:12, Heming Cui <heming at cs.columbia.edu> 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 > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
