[fix] Fix isStuck

UnitTestBot · Nov 3, 2023 · 9f054a9 · 9f054a9
1 parent 01ddb65
commit 9f054a9
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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()) {