[klee-dev] Path Search Heuristics

[Sean Bartell]

Zhiyi Zhang on 2015-05-24:
>1, It seems that KLEE can NOT generate test cases when I only used
>search==nurs:covnew as the path search heuristic. Moreover, when using
>search==nurs:md2u, search==nurs:icnt, search==nurs:cpicnt or
>search==nurs:qc as  as the only path search heuristic,  KLEE also does NOT
>generate test cases. I am confused why this phenomenon happens?

How does it fail? Does it crash with an error message, or does it just keep 
running without printing anything?

>2, The default search heuristic for KLEE is "random-path interleaved with
>nurs:covnew". What is the meaning of "interleaved"? Does it mean randomly
>selecting one search heuristic from such two search heuristics when
>searching a path?

Yes, except that it isn't random. The "interleaved" searcher just alternates 
between using two other searchers. "nurs:covnew" and other searchers can always 
choose a state.
-------------- next part --------------
HTML attachment scrubbed and removed