Hi all, I am reading KLEE’s source code and find that if I set “-max-fork=n” when KLEE reach its fork limit n, it will still symbolic executing the program. In my understanding, when KLEE stops forking, there is no need to invoke SMT solver to check which branch is reachable or not, therefore it is also unnecessary to symbolic executing the program in order to set up more constraints. Thus I would like to know why KLEE not concretely running the program after reaching fork limit?
Thanks!
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
