diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 7bfeece2f6f35e88c4557db2ecafe4c684a1198d..4a395912a6b9dc92a9828fc90bed421baf009c97 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -37,7 +37,6 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
       TypingPhase                            andThen
       synthesis.ConversionPhase              andThen
       CheckADTFieldsTypes                    andThen
-      InjectAsserts                          andThen
       InliningPhase
 
     val pipeX = if(desugarXLang) {
@@ -50,6 +49,7 @@ class PreprocessingPhase(desugarXLang: Boolean = false) extends LeonPhase[Progra
     val phases =
       pipeBegin andThen
       pipeX andThen
+      InjectAsserts andThen
       FunctionClosure andThen
       AdaptationPhase andThen
       debugTrees("Program after pre-processing")
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index a2ba463a6519a4c10e224c583263b805b4f660d7..4e126827bd6cf352692c43e8433857b8894615d4 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -30,8 +30,6 @@ object InjectAsserts extends SimpleLeonPhase[Program, Program] {
             Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), i).setPos(i),
             v
           ).setPos(e))
-        case e @ ArrayUpdate(a, i, _)  =>
-          Some(Assert(indexUpTo(i, ArrayLength(a)), Some("Array index out of range"), e).setPos(e))
         case e @ MapApply(m,k) =>
           Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ffcc9e3621ede9050a85b19ce2651d57a71b3680
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array6 {
+
+  def test(): Int = {
+    var c = 1
+    val a = Array(0,1,2,3)
+    a({
+      if(a(0) == 0) { c = c+1; 1}
+      else { c = c+2; 2}
+    }) = { c = c*2; -1}
+    c
+  } ensuring(res => res == 4)
+
+}