From 37cc23f4112c61bddcb0f1e5d152c5a9bc174918 Mon Sep 17 00:00:00 2001
From: Matthias Heizmann <heizmann@informatik.uni-freiburg.de>
Date: Sun, 2 Oct 2022 00:08:14 +0200
Subject: [PATCH] bugfix in backtranslation (related to
 https://github.com/ultimate-pa/ultimate/issues/596#issuecomment-1262718594)

---
 .../buchiprogramproduct/ProductBacktranslator.java         | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/trunk/source/BuchiProgramProduct/src/de/uni_freiburg/informatik/ultimate/buchiprogramproduct/ProductBacktranslator.java b/trunk/source/BuchiProgramProduct/src/de/uni_freiburg/informatik/ultimate/buchiprogramproduct/ProductBacktranslator.java
index 6d8ef496177..446119cd6bb 100644
--- a/trunk/source/BuchiProgramProduct/src/de/uni_freiburg/informatik/ultimate/buchiprogramproduct/ProductBacktranslator.java
+++ b/trunk/source/BuchiProgramProduct/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