assert should be injected after xlang

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")

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))
 

src/test/resources/regression/verification/xlang/valid/Array6.scala

+/* 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)
+
+}