diff options
| -rw-r--r-- | lib/Core/Searcher.cpp | 2 | ||||
| -rw-r--r-- | test/regression/2020-04-11-batching-search-zero-time-budget.c | 16 |
2 files changed, 17 insertions, 1 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 080c31aa..f5d6543f 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -423,7 +423,7 @@ ExecutionState &BatchingSearcher::selectState() { (time::getWallTime() - lastStartTime) > timeBudget)) || ((instructionBudget > 0) && (stats::instructions - lastStartInstructions) > instructionBudget)) { - if (lastState) { + if (lastState && timeBudget.toSeconds() > 0) { time::Span delta = time::getWallTime() - lastStartTime; auto t = timeBudget; t *= 1.1; diff --git a/test/regression/2020-04-11-batching-search-zero-time-budget.c b/test/regression/2020-04-11-batching-search-zero-time-budget.c new file mode 100644 index 00000000..46043f31 --- /dev/null +++ b/test/regression/2020-04-11-batching-search-zero-time-budget.c @@ -0,0 +1,16 @@ +// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --use-batching-search --batch-time=0 --batch-instructions=1 %t.bc 2>&1 | FileCheck %s + +#include <time.h> + +#include "klee/klee.h" + +int main(void) { + for (int i = 0; i < 10; ++i) { + struct timespec ts = {.tv_sec = 0, .tv_nsec = 10000000}; // 10 ms + nanosleep(&ts, NULL); + } + // CHECK-NOT: increased time budget + return 0; +} |