If finding an assertion fail in one execution, KLEE will report it, then ignore it and keep searching for other executions. Then it comes to my question: is there any configuration or trick to force KLEE to stop searching when finding an assertion fail? Or do I have to make modification on source code and re-build KLEE to implement it? Hope for inspiring solutions. Thanks in advance!
KLEE does not exit if a bug is found in the analyzed application by default. On the other hand, KLEE implicitly exits on some failures. This behaviour can be changed by the following options:
-exit-on-error - Exit on the first arbitrary error.
-exit-on-error-type=TYPE - Exit on the first error of type TYPE. This parameter can be repeated to exit after more types.
https://klee.github.io/docs/options/#making-klee-exit-on-events