diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 989942f2232d49afd946d9c05d5f0f5506b19c4f..7ab5925cebf63dd462db2627a45299e46e05978a 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -242,7 +242,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
         val fd = tfd.fd
         state.funDefsMapping.get(fd) match { 
           case Some((newFd, modifiedVars)) => {
-            val newInvoc = FunctionInvocation(newFd.typed, args ++ modifiedVars.map(id => id.toVariable)).setPos(fi)
+            val newInvoc = FunctionInvocation(newFd.typed, recArgs ++ modifiedVars.map(id => id.toVariable)).setPos(fi)
             val freshNames = modifiedVars.map(id => id.freshen)
             val tmpTuple = FreshIdentifier("t", newFd.returnType)
 
@@ -252,7 +252,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
                   Let(p._1, TupleSelect(tmpTuple.toVariable, p._2 + 2), b))
               ))
             }
-            val newMap = modifiedVars.zip(freshNames).toMap ++ argFun
+            val newMap = argFun ++ modifiedVars.zip(freshNames).toMap
 
             (TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
           }
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f263529653486ee5477b9fd1934760bcdc737d15
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder3 {
+
+  def leftToRight(n: BigInt): BigInt = {
+    require(n > 0)
+
+    var a = BigInt(0)
+
+    def nested(x: BigInt, y: BigInt): Unit = {
+      a = x + y
+    }
+
+    nested({a += 10; a}, {a *= 2; a})
+    a
+
+  } ensuring(_ == 30)
+
+}