[klee-dev] When KLEE finishing forking

[XIE Xuan]

Hi all,

I would like to know what is KLEE doing when reaching fork limit but not reaching time limit.
I am trying the second tutorial here(http://klee.github.io/tutorials/testing-regex/).

When I set fork limit to 6000 and time limit to 10 seconds, that is using command `klee -max-forks=6000 -max-time=10 Regexp.bc ` it generate:
KLEE: done: completed paths = 6001
KLEE: done: generated tests = 5321
However, when I set fork limit to 6000 and time limit to 6 seconds, that is using command `klee -max-forks=6000 -max-time=6 Regexp.bc ` it still generate same number of paths and test. I am wondering what KLEE is doing after reaching fork limit. If it is solving the constraint for different path, then it shouldn’t generate the same number of test for two different configuration. Am I understand wrong?

Thank you very much!
-------------- next part --------------
HTML attachment scrubbed and removed