Fixing a bug: off-by-one error in the executed trace checking.
authorrtrimana <rtrimana@uci.edu>
Fri, 27 Mar 2020 23:49:04 +0000 (16:49 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 27 Mar 2020 23:49:04 +0000 (16:49 -0700)
src/main/gov/nasa/jpf/listener/StateReducer.java

index 91c0b11..94b78f8 100644 (file)
@@ -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();