From: rtrimana <rtrimana@uci.edu>
Date: Fri, 14 Feb 2020 18:32:06 +0000 (-0800)
Subject: Fixing an out of bound bug.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=b49d73a21fbf80e60a3ce095b4e2f49d07bede52

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 4740583..93043fa 100644
--- 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 (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