From: rtrimana <rtrimana@uci.edu>
Date: Fri, 27 Mar 2020 23:49:04 +0000 (-0700)
Subject: Fixing a bug: off-by-one error in the executed trace checking.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=24a0385288ecaa3a5027a28d0484e5fe2fee2301

Fixing a bug: off-by-one error in the executed trace checking.
---

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 91c0b11..94b78f8 100644
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -602,9 +602,7 @@ public class StateReducer extends ListenerAdapter {
 
     // When we see a choice list shorter than the upper bound, e.g., [3,2] for choices 0,1,2, and 3,
     //  then we have to pad the beginning before we store it, because [3,2] actually means [0,1,3,2]
-    // First, calculate the difference between this choice list and the upper bound
-    //  The actual list doesn't include '-1' at the end
-    int actualListLength = newChoiceList.length - 1;
+    int actualListLength = newChoiceList.length;
     int diff = maxUpperBound - actualListLength;
     StringBuilder sb = new StringBuilder();
     // Pad the beginning if necessary
@@ -613,7 +611,7 @@ public class StateReducer extends ListenerAdapter {
     }
     // Then continue with the actual choice list
     // We don't include the '-1' at the end
-    for (int i = 0; i < newChoiceList.length - 1; i++) {
+    for (int i = 0; i < newChoiceList.length; i++) {
       sb.append(newChoiceList[i]);
     }
     return sb.toString();