Inliner backtranslation: fix handling of old() variables

ultimate-pa · Dec 17, 2024 · 2113945 · 2113945
1 parent f54f23d
commit 2113945
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/...nformatik/ultimate/boogie/procedureinliner/backtranslation/ExpressionBacktranslation.java b/...nformatik/ultimate/boogie/procedureinliner/backtranslation/ExpressionBacktranslation.java
@@ -144,7 +144,7 @@ public Expression processExpression(final Expression expr) {
 			Expression newExpr = new IdentifierExpression(location, type, translatedId, translatedDeclInfo);
 			ModelUtils.copyAnnotations(expr, newExpr);
 			if (mapping.getGlobalInOldExprOfProc() != null) {
-				newExpr = new UnaryExpression(location, type, Operator.OLD, idExpr);
+				newExpr = new UnaryExpression(location, type, Operator.OLD, newExpr);
 			}
 			if (translatedDeclInfo.getStorageClass() == GLOBAL || translatedDeclInfo.getStorageClass() == QUANTIFIED
 					|| mActiveProcedures.contains(translatedDeclInfo.getProcedure())) {