diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7a00cb7f8d128a6b9d495950d5cd0bc444093c7c..2f8b897962c556cc1c86ad615c15f21887a44f81 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -230,6 +230,15 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
 
       //a function invocation can update variables in scope.
       case fi@FunctionInvocation(tfd, args) =>
+
+
+        val (recArgs, argScope, argFun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
+          val (accArgs, accScope, accFun) = acc
+          val (argVal, argScope, argFun) = toFunction(arg)
+          val newScope = (body: Expr) => argScope(replaceNames(argFun, accScope(body)))
+          (argVal +: accArgs, newScope, argFun ++ accFun)
+        })
+
         val fd = tfd.fd
         state.funDefsMapping.get(fd) match { 
           case Some((newFd, modifiedVars)) => {
@@ -238,16 +247,17 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
             val tmpTuple = FreshIdentifier("t", newFd.returnType)
 
             val scope = (body: Expr) => {
-              Let(tmpTuple, newInvoc,
+              argScope(Let(tmpTuple, newInvoc,
                 freshNames.zipWithIndex.foldRight(body)((p, b) =>
                   Let(p._1, TupleSelect(tmpTuple.toVariable, p._2 + 2), b))
-              )
+              ))
             }
-            val newMap = modifiedVars.zip(freshNames).toMap
+            val newMap = modifiedVars.zip(freshNames).toMap ++ argFun
 
             (TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
           }
-          case None => (fi, x => x, Map())
+          case None => 
+            (FunctionInvocation(tfd, recArgs).copiedFrom(fi), argScope, argFun)
         }
         
 
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8ef668a2afeb61a6b305831358a65e675bf670ed
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
@@ -0,0 +1,22 @@
+object FunInvocEvaluationOrder1 {
+
+  def test(): Int = {
+
+    var res = 10
+    justAddingStuff({
+      res += 1
+      res
+    }, {
+      res *= 2
+      res
+    }, {
+      res += 10
+      res
+    })
+
+    res
+  } ensuring(_ == 32)
+
+  def justAddingStuff(x: Int, y: Int, z: Int): Int = x + y + z
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12090f0f3fad0a5fcf2451e30fdb6f25bb09c590
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder2 {
+
+  def leftToRight(n: BigInt): BigInt = {
+    require(n > 0)
+
+    var a = BigInt(0)
+
+    def nested(x: BigInt, y: BigInt): BigInt = {
+      require(y >= x)
+      x + y
+    }
+
+    nested({a += 10; a}, {a *= 2; a})
+
+  } ensuring(_ == 30)
+
+}