diff options
author | Julian Büning <julian.buening@comsys.rwth-aachen.de> | 2020-04-11 16:43:01 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-06-05 17:13:21 +0100 |
commit | d3aee9c0e619fa097e296de81de93a09aaab82f2 (patch) | |
tree | 01bd41526ea0cbcb05f5092870fac47be9b409f4 /lib/Core | |
parent | 3c42e214fb2ec4a101dd1e91e2d8c1ce4983a569 (diff) | |
download | klee-d3aee9c0e619fa097e296de81de93a09aaab82f2.tar.gz |
fix BatchingSearcher's disabled time budget
The functionality of the batching searcher that increases the time budget if it is shorter than the time between two calls to `selectState()` ignored the disabled time budget. Effectively, the batching searcher thus picks a very arbitrary time budget on its own.
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Searcher.cpp | 2 |
1 files changed, 1 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; |