[klee-dev] [Question] What is the correct/efficient way to implement a separate execution without affecting the normal execution in KLEE?

[Frank Busse]

Dear Haoxin,


On Tue, 26 Mar 2024 07:51:13 +0000
TU Haoxin <haoxintu.2020 at phdcs.smu.edu.sg> wrote:

> In the first normal execution, I don't know which state is good to
> explore so I randomly select one (say "C" is selected). Then, I want
> to use a "simulation" run (a separate execution from a normal
> execution ) to evaluate the "value/reward" of this state based on the
> results of the simulation run. After the simulation execution
> terminates, KLEE will switch to normal execution.

I think it would be helpful if you would explain how a simulation run
defers from a normal exploration in KLEE. Especially, how would you
determine what branches to take?


Kind regards,

Frank