diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 6b7f7cc6ee3c00827289313ed60e111b6ec3a640..506cb86ce95bb044f709e23b6483ec1dcfb6ff7e 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -155,7 +155,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
           val (rVal, rScope, rFun) = toFunction(e)
           val scope = (body: Expr) => {
             rVal match {
-              case FunctionInvocation(tfd, args) if tfd.hasPrecondition =>
+              case FunctionInvocation(tfd, args) =>
                 rScope(replaceNames(rFun, Let(FreshIdentifier("tmp", tfd.returnType), rVal, accScope(body))))
               case _ =>
                 rScope(replaceNames(rFun, accScope(body)))