[klee-dev] Effect of --optimize

[Frank Busse]

Hi,


On Thu, 23 Sep 2021 17:03:03 +0100
Eduardo R B Marques <ebmarques at fc.up.pt> wrote:

> $ klee --optimize --only-output-states-covering-new Regexp.bc
> …
> KLEE: Using STP solver backend
> 
> KLEE: done: total instructions = 5
> KLEE: done: completed paths = 1
> KLEE: done: partially completed paths = 0
> KLEE: done: generated tests = 1

This is a bug. The call of match() is completely removed from main() in
the bitcode. Using "--klee-call-optimisation=false" might help.


Kind regards,

Frank