Fixing a bug: VOD graph traversal should continue with the next neighbor when there...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 7d5546c2be70d4028d79069dce39edb81b6cbb85..f9d79c5a27d160515657424b83a7fd88388afa4c 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -796,8 +796,8 @@ public class DPORStateReducer extends ListenerAdapter {
         if (choice == currEvent) {
           return true;
         }
         if (choice == currEvent) {
           return true;
         }

-        if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it
-          return false;
+        if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration
+          continue;

         }
         // Continue searching
         visitedChoice.add(choice);
         }
         // Continue searching
         visitedChoice.add(choice);