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.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
