[klee-dev] Klee Dump States Question

[eric.rizzi at huskers.unl.edu]

Hello,

I have been working with Klee for the past few weeks and I have a question related to what happens when Klee reaches it's timeout (-max-time) and dumps it's states.

It seems that this "wrapping up" period requires significant time, often exceeding the initial timeout.  In addition, when examining the output sent to the solver, the number of queries being generated is significantly higher after the timeout than before.

My question is, why is this happening?  It seems that upon wrapping up, the states on the edge of the exploration should be solved for, creating one test that will pass through each of these states.  My intuition, however, is clearly wrong.

In case it helps, I used the following command line to run Klee

% klee --libc=uclibc --posix-runtime --use-query-log=solver:smt2 --max-time=1000 program.bc --sym-args 1 3 12 --sym-files 2 100

Thanks,
Eric Rizzi
-------------- next part --------------
HTML attachment scrubbed and removed