diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 02a21c50849b20d0a93fc4b400a27ff8b78ae05d..1c1e52b17bc57537128e2186f342937aab62ecd0 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -13,7 +13,7 @@ object Main {
       utils.TypingPhase,
       utils.FileOutputPhase,
       purescala.RestoreMethods,
-      xlang.ArrayTransformation,
+      xlang.AntiAliasingPhase,
       xlang.EpsilonElimination,
       xlang.ImperativeCodeElimination,
       xlang.FixReportLabels,
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index d237c89d5089c13b4a8c6aa50e04dc7c3754e0fd..f1ea90043736d1ea59a5ae0d9747e15905509cd6 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -63,8 +63,8 @@ object AntiAliasingPhase extends TransformationPhase {
   /*
    * Create a new FunDef for a given FunDef in the program.
    * Adapt the signature to express its effects. In case the
-   * function has no effect, this will still introduce a fresh
-   * FunDef as the body might have to be updated anyway.
+   * function has no effect, this will still return the original
+   * fundef.
    */
   private def updateFunDef(fd: FunDef, effects: Effects)(ctx: LeonContext): FunDef = {
 
@@ -87,13 +87,13 @@ object AntiAliasingPhase extends TransformationPhase {
     //  case _ => ()
     //})
 
-    val newReturnType: TypeTree = if(aliasedParams.isEmpty) fd.returnType else {
-      tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
+    if(aliasedParams.isEmpty) fd else {
+      val newReturnType: TypeTree = tupleTypeWrap(fd.returnType +: aliasedParams.map(_.getType))
+      val newFunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, newReturnType)
+      newFunDef.addFlags(fd.flags)
+      newFunDef.setPos(fd)
+      newFunDef
     }
-    val newFunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, newReturnType)
-    newFunDef.addFlags(fd.flags)
-    newFunDef.setPos(fd)
-    newFunDef
   }
 
   private def updateBody(fd: FunDef, effects: Effects, updatedFunDefs: Map[FunDef, FunDef], varsInScope: Map[FunDef, Set[Identifier]])
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
deleted file mode 100644
index 7c66bc3eb6aafb5512b65731a7f0193dece30a8d..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-/* Copyright 2009-2016 EPFL, Lausanne */
-
-package leon.xlang
-
-import leon.UnitPhase
-import leon.LeonContext
-import leon.purescala.Definitions._
-import leon.purescala.Expressions._
-import leon.purescala.ExprOps.simplePostTransform
-import leon.purescala.Extractors.IsTyped
-import leon.purescala.Types.ArrayType
-import leon.xlang.Expressions._
-
-object ArrayTransformation extends UnitPhase[Program] {
-
-  val name = "Array Transformation"
-  val description = "Remove side-effectful array updates"
-
-  def apply(ctx: LeonContext, pgm: Program) = {
-    pgm.definedFunctions.foreach(fd =>
-      fd.fullBody = simplePostTransform {
-        case up@ArrayUpdate(a, i, v) =>
-          val ra@Variable(id) = a
-          Assignment(id, ArrayUpdated(ra, i, v).setPos(up)).setPos(up)
-
-        case l@Let(i, IsTyped(v, ArrayType(_)), b) =>
-          LetVar(i, v, b).setPos(l)
-
-        case e =>
-          e
-      }(fd.fullBody)
-    )
-  }
-
-}
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 89a5ad4cde356d456f73d7a604da5c8096947501..de75b7a29c0494ba4052aefe9fcb4f974dd128a2 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -21,7 +21,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
   def apply(ctx: LeonContext, pgm: Program): Unit = {
     for {
       fd <- pgm.definedFunctions
-      body <- fd.body
+      body <- fd.body if exists(requireRewriting)(body)
     } {
       val (res, scope, _) = toFunction(body)(State(fd, Set(), Map()))
       fd.body = Some(scope(res))
@@ -351,4 +351,12 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
     })(expr)
   }
 
+  private def requireRewriting(expr: Expr) = expr match {
+    case (e: Block) => true
+    case (e: Assignment) => true
+    case (e: While) => true
+    case (e: LetVar) => true
+    case _ => false
+  }
+
 }
diff --git a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
index 51c2721d03074b83db148f2f9d3a24b3eeb2e4d9..54e298a226704a78fb99abc445e55df8895bc98f 100644
--- a/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
+++ b/src/main/scala/leon/xlang/XLangDesugaringPhase.scala
@@ -12,7 +12,6 @@ object XLangDesugaringPhase extends LeonPhase[Program, Program] {
 
   override def run(ctx: LeonContext, pgm: Program): (LeonContext, Program) = {
     val phases =
-      //ArrayTransformation andThen
       AntiAliasingPhase andThen
       EpsilonElimination andThen
       ImperativeCodeElimination