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
/klee/klee/blob/fc50ab32349a4cc61980ba5b97bfa7c3961ce964/lib/Core/Executor.cpp#L975)
That is the point I don’t understand.
Thanks for any help!
From: on behalf of XIE Xuan
Date: Monday, May 25, 2020 at 11:32 AM
To: "klee-dev@imperial.ac.uk"
Subject: [klee-dev] Why KLEE still symbolic
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
