[klee-dev] KLEE generated only one path whereas program has two

[Dan Liew]

> But the output from KLEE indicated that it completed only one path whereas
> the program clearly has two paths. Can anyone please explain why this
> happened ?

Remember that KLEE executes LLVM IR, not C! You should look at the
LLVM IR. If you look (see ``klee-last/assembly.ll``) you'll see that
the branch has been lowered
to a select instruction (i.e. an if then else instruction). This
happens due to the running the pass created by
``createCFGSimplificationPass()`` in ``KModule::prepare(...)``