[klee-dev] Why KLEE still symbolic executing program after reaching max-fork?

[Cristian Cadar]

Hi,

This was the simplest way to implement --max-forks.  I agree you could 
improve this, depending also on what you want to achieve.

Best,
Cristian

On 25/05/2020 10:31, XIE Xuan wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>