also apply the transformation to precondition and postcondition

src/main/scala/leon/ArrayTransformation.scala

@@ -30,8 +30,8 @@ object ArrayTransformation extends Pass {
           val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
           freshFunDef.fromLoop = fd.fromLoop
           freshFunDef.parent = fd.parent
-          freshFunDef.precondition = fd.precondition
-          freshFunDef.postcondition = fd.postcondition
+          freshFunDef.precondition = fd.precondition.map(transform)
+          freshFunDef.postcondition = fd.postcondition.map(transform)
           freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
           fd2fd += (fd -> freshFunDef)
           freshFunDef
@@ -160,8 +160,8 @@ object ArrayTransformation extends Pass {
             val freshFunDef = new FunDef(freshFunName, fd.returnType, newArgs)
             freshFunDef.fromLoop = fd.fromLoop
             freshFunDef.parent = fd.parent
-            freshFunDef.precondition = fd.precondition
-            freshFunDef.postcondition = fd.postcondition
+            freshFunDef.precondition = fd.precondition.map(transform)
+            freshFunDef.postcondition = fd.postcondition.map(transform)
             freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
             fd2fd += (fd -> freshFunDef)
             freshFunDef

testcases/regression/valid/Array5.scala

 import leon.Utils._
 
-object Array4 {
+object Array5 {
 
   def foo(a: Array[Int]): Int = {
     var i = 0

testcases/regression/valid/Array6.scala

+import leon.Utils._
+
+object Array6 {
+
+  def foo(a: Array[Int]): Int = {
+    require(a.length > 2 && a(2) == 5)
+    a(2)
+  } ensuring(_ == 5)
+
+  def bar(): Int = {
+    val a = Array.fill(5)(5)
+    foo(a)
+  }
+
+}