[klee-dev] Klee skips some conditional branch instructions in the actual bitcode file

[Mohammad Wamiq Saifi]

Hi,

I am doing a replay path using klee on a bitcode file without any
optimization options. When printing the instruction trace using
"-debug-print-instructions" options klee seems to skip a conditional branch
which forces it to follow the undesired path (different from replay path).
I don't understand why is klee showing such a behaviour.

Are there any optimizations which I need to turn off (I have tried using
"-disable-opt") ?

Is there a way to disable all such optimizations/checks (like
"check-divide-zero", "check-overshift") which could affect replay-path  and
run klee on the bitcode file "as is" ?

Thanks & Regards
Wamiq
-------------- next part --------------
HTML attachment scrubbed and removed