Hello guys. I recently read article *Path-based Inductive Synthesis for Program Inversion *and found it very insightful. However, I have encountered some questions regarding one of the principles discussed in the paper about symbolic execution. I am writing to seek clarification on this point.
As in Cond&Loop rule: Rule COND non-deterministically executes one of its branches. Rule LOOP unrolls a loop one time. Is that means in symbolic execution, for each iteration of the loop, it unrolls the loop into an “if” statement. Then, it randomly chooses either to execute the loop body or to jump to the else branch (exit the loop). Or it just unroll the loop again and again util it not meet the requirements of “While” anymore?
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
