Hi Charitha,
I think you would need to do the modification in Executor::fork().
You would notice within that function there is the following three lines:
solver->setTimeout(timeout);
bool success = solver->evaluate(current, condition, res);
solver->setTimeout(0);
I would try to replace those
Hi,
I want to implement a search strategy in KLEE.
If I know some branch is feasible from prior knowledge (say I learn that
for a some br instruction the true branch is always feasible),
How can I change KLEE to avoid calling the solver in Executor.cpp (in
Instruction::Br)
and just guide
