Fixing an out of bound bug.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 474058355c1f7f82f00403cf67705e4d406fd8a5..93043fa33d7b9a09491bdb3ac33df09f44e014d3 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -300,8 +300,8 @@ public class StateReducer extends ListenerAdapter {
     if (stateReductionMode) {
       // Update vodGraph
       int currChoice = choiceCounter - 1;
     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
         return;
       }
       // When current choice is 0, previous choice could be -1