diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 7ae7d692cb..9e74c4ef37 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -509,9 +509,9 @@ class ExecutionState { } inline bool isStuck(unsigned long long bound) const { - if (depth == 1) + if (depth == 0) return false; - return isCycled(bound) && depth > klee::util::ulog2(bound); + return isCycled(bound) && klee::util::ulog2(depth) > bound; } bool isCoveredNew() const { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fd4d9333be..b4e17bf9e6 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -4415,7 +4415,7 @@ void Executor::executeStep(ExecutionState &state) { if (targetManager->isTargeted(state) && state.targets().empty()) { terminateStateEarlyAlgorithm(state, "State missed all it's targets.", StateTerminationType::MissedAllTargets); - } else if (state.isStuck(MaxCycles)) { + } else if (state.isCycled(MaxCycles)) { terminateStateEarly(state, "max-cycles exceeded.", StateTerminationType::MaxCycles); } else { diff --git a/lib/Core/TargetManager.cpp b/lib/Core/TargetManager.cpp index 23ad1347e8..9dcaedcd86 100644 --- a/lib/Core/TargetManager.cpp +++ b/lib/Core/TargetManager.cpp @@ -135,7 +135,7 @@ void TargetManager::updateReached(ExecutionState &state) { void TargetManager::updateTargets(ExecutionState &state) { if (guidance == Interpreter::GuidanceKind::CoverageGuidance) { - if (targets(state).empty() && state.isCycled(MaxCyclesBeforeStuck)) { + if (targets(state).empty() && state.isStuck(MaxCyclesBeforeStuck)) { state.setTargeted(true); } if (isTargeted(state) && targets(state).empty()) {