Fixing an out of bound bug.
[jpf-core.git] / src / main / gov / nasa / jpf / listener / StateReducer.java
index 4740583..93043fa 100644 (file)
@@ -300,8 +300,8 @@ public class StateReducer extends ListenerAdapter {
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
-      if (currChoice < 0 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
-        // Current choice has to be at least 0 (initial case can be -1)
+      if (currChoice < 0 || currChoice > choices.length - 1 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
+        // Handle all corner cases (e.g., out of bound values)
         return;
       }
       // When current choice is 0, previous choice could be -1