From: UCI Networking Group <ucinetworkinggroup@UCIs-MacBook-Pro.local>
Date: Fri, 11 Dec 2020 00:01:36 +0000 (-0800)
Subject: Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=461ece5d48c8a96e967b2670802406d1d4157df3

Fixing a potential bug: if statement that contains updateBacktrackSetsFromGraph was only called once.
---

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a0abd98..82f3db8 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -752,8 +752,8 @@ public class DPORStateReducer extends ListenerAdapter {
     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
     boolean terminate = false;
     for(Integer stateId : justVisitedStates) {
-      // We only flip the value of terminate once ...
-      if (!terminate && prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+      // We perform updates on backtrack sets for every
+      if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
         updateBacktrackSetsFromGraph(stateId);
         terminate = true;
       }