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 91c0b11cb0060fd65b75500470db2522fd387549..94b78f8ea866da2629abb0a01463c51a88c894b0 100644 (file)
--- 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]
 
     // 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
     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
     }
     // 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();
       sb.append(newChoiceList[i]);
     }
     return sb.toString();