Fixing bug: 1) pushed transition should have been the predecessor transition after...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 70d89356d1bce74435dbf8d56373854da6b51b24..5b0359ed5a92198f351200cda526b7ab573b3e2e 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -1182,8 +1182,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // Check if a conflict is found
       if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
         createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
-        newConflictChoice = conflictChoice;
-        newConflictExecution = conflictExecution;
+        newConflictChoice = predecessorChoice;
+        newConflictExecution = predecessorExecution;
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,