fix bug in testcase and support the complete language in ArrayTransformation

src/main/scala/leon/ArrayTransformation.scala

@@ -116,9 +116,23 @@ object ArrayTransformation extends Pass {
       LetVar(id, er, br)
     }
 
-    //case ite@IfExpr(cond, tExpr, eExpr) => 
+    case ite@IfExpr(c, t, e) => {
+      val rc = transform(c)
+      val rt = transform(t)
+      val re = transform(e)
+      IfExpr(rc, rt, re).setType(rt.getType)
+    }
+
+    case m @ MatchExpr(scrut, cses) => {
+      val scrutRec = transform(scrut)
+      val csesRec = cses.map{
+        case SimpleCase(pat, rhs) => SimpleCase(pat, transform(rhs))
+        case GuardedCase(pat, guard, rhs) => GuardedCase(pat, transform(guard), transform(rhs))
+      }
+      val tpe = csesRec.head.rhs.getType
+      MatchExpr(scrutRec, csesRec).setType(tpe).setPosInfo(m)
+    }
 
-    //case m @ MatchExpr(scrut, cses) => 
     //case LetDef(fd, b) => 
 
     case n @ NAryOperator(args, recons) => recons(args.map(transform)).setType(n.getType)

testcases/regression/valid/Array4.scala

+import leon.Utils._
+
 object Array4 {
 
   def foo(a: Array[Int]): Int = {
-    a(2)
-  } ensuring(_ == 3)
+    var i = 0
+    var sum = 0
+    (while(i < a.length) {
+      sum = sum + a(i)
+      i = i + 1
+    }) invariant(i >= 0)
+    sum
+  }
 
 }