bugfix in backtranslation (related to #596 (comment))

ultimate-pa · Oct 1, 2022 · 37cc23f · 37cc23f
1 parent cf36bb6
commit 37cc23f
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/...ct/src/de/uni_freiburg/informatik/ultimate/buchiprogramproduct/ProductBacktranslator.java b/...ct/src/de/uni_freiburg/informatik/ultimate/buchiprogramproduct/ProductBacktranslator.java
@@ -82,7 +82,7 @@ public ProductBacktranslator(final Class<? extends IIcfgTransition<IcfgLocation>
 				continue;
 			}
 			newTrace.add(mappedEdge);
-			addProgramState(i, newValues, programExecution.getProgramState(i));
+			addProgramState(newTrace.size() - 1, newValues, programExecution.getProgramState(i));
 			if (oldBranchEncoders != null) {
 				newBranchEncoders.add(oldBranchEncoders[i]);
 			}
@@ -98,7 +98,10 @@ public ProductBacktranslator(final Class<? extends IIcfgTransition<IcfgLocation>
 
 	private static void addProgramState(final Integer i, final Map<Integer, ProgramState<Term>> newValues,
 			final ProgramState<Term> programState) {
-		newValues.put(i, programState);
+		final ProgramState<Term> oldProgramState = newValues.put(i, programState);
+		if ((oldProgramState != null)) {
+			throw new AssertionError("Must not overwrite existing state.");
+		}
 	}
 
 	@Override