diff --git a/trunk/source/BoogieProcedureInliner/src/de/uni_freiburg/informatik/ultimate/boogie/procedureinliner/backtranslation/ExpressionBacktranslation.java b/trunk/source/BoogieProcedureInliner/src/de/uni_freiburg/informatik/ultimate/boogie/procedureinliner/backtranslation/ExpressionBacktranslation.java index 5457af39aa..25345f4233 100644 --- a/trunk/source/BoogieProcedureInliner/src/de/uni_freiburg/informatik/ultimate/boogie/procedureinliner/backtranslation/ExpressionBacktranslation.java +++ b/trunk/source/BoogieProcedureInliner/src/de/uni_freiburg/informatik/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())) {