diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 9c2623b8dba9815f8e75b89e6a2d4a1eccb86180..3b80989e6f70f893b86bedaaf7632823e9015159 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -124,9 +124,18 @@ object AntiAliasingPhase extends TransformationPhase {
         val freshBody = replaceFromIDs(rewritingMap.map(p => (p._1, p._2.toVariable)), body) 
         val explicitBody = makeSideEffectsExplicit(freshBody, fd, freshLocalVars, effects, updatedFunDefs, varsInScope)(ctx)
 
+        //only now we rewrite variables that stil refer to original higher order functions
+        val ftRewritings: Map[Identifier, Identifier] =
+          fd.params.zip(newFunDef.params).filter({
+            case (ValDef(IsTyped(oid, oft)), ValDef(IsTyped(nid, nft))) if oid != nft => true
+            case _ => false
+          }).map(p => (p._1.id, p._2.id)).toMap
+        val explicitBody2 = replaceFromIDs(ftRewritings.map(p => (p._1, p._2.toVariable)), explicitBody)
+              
+
         //WARNING: only works if side effects in Tuples are extracted from left to right,
         //         in the ImperativeTransformation phase.
-        val finalBody: Expr = Tuple(explicitBody +: freshLocalVars.map(_.toVariable))
+        val finalBody: Expr = Tuple(explicitBody2 +: freshLocalVars.map(_.toVariable))
 
         freshLocalVars.zip(aliasedParams).foldLeft(finalBody)((bd, vp) => {
           LetVar(vp._1, Variable(vp._2), bd)
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..64829e949d71fdfc93d82c4da88bb3fa3b54d4a8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams5.scala
@@ -0,0 +1,23 @@
+object HigherOrderFunctionsMutableParams5 {
+
+  case class A(var x: BigInt)
+
+  def repeat(f: (A, BigInt) => Unit, n: BigInt, a: A): Unit = {
+    require(n >= 0)
+    if(n > 0) {
+      f(a, n)
+      repeat(f, n-1, a)
+    }
+  }
+
+  def fImpl(a: A, n: BigInt): Unit = {
+    a.x += 1
+  }
+
+  def test(): BigInt = {
+    val a = A(0)
+    repeat(fImpl, 3, a)
+    a.x
+  } ensuring(_ == 3)
+
+}