diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala index a61605287496ac48d57036f27940fbe3065a9f2f..d25965ede6a34f8de6206ec1b38cb0e6381b3d41 100644 --- a/src/main/scala/leon/ArrayTransformation.scala +++ b/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) diff --git a/testcases/regression/valid/Array4.scala b/testcases/regression/valid/Array4.scala index 479f243ba3962304e8be552924ed4a5275622db4..fd76e02faa83f8fd1bda5fef7c91e7df7fc29864 100644 --- a/testcases/regression/valid/Array4.scala +++ b/testcases/regression/valid/Array4.scala @@ -1,7 +1,15 @@ +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 + } }