diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 56239d319dca67c9614f0e7d9dd97a7640c8da49..8a6fd5bffd1a7c6a9a6a9b6fdde5e8bd3598f940 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -64,12 +64,14 @@ object FunctionClosure extends Pass {
newFunDef.postcondition = freshPostcondition
pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
- val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable))))))
+ //val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclFreshIds.map(_.toVariable))))))
+ val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable))))))
newFunDef.body = freshBody
pathConstraints = pathConstraints.tail
- val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd ->
- ((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable)))))
+ //val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd ->
+ // ((newFunDef, extraVarDeclOldIds.map(id => id2freshId.get(id).getOrElse(id).toVariable)))))
+ val freshRest = functionClosure(rest, bindedVars, id2freshId, fd2FreshFd + (fd -> ((newFunDef, extraVarDeclOldIds.map(_.toVariable)))))
freshRest.setType(l.getType)
}
case l @ Let(i,e,b) => {
@@ -99,7 +101,8 @@ object FunctionClosure extends Pass {
case fi @ FunctionInvocation(fd, args) => fd2FreshFd.get(fd) match {
case None => FunctionInvocation(fd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd))).setPosInfo(fi)
case Some((nfd, extraArgs)) =>
- FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++ extraArgs).setPosInfo(fi)
+ FunctionInvocation(nfd, args.map(arg => functionClosure(arg, bindedVars, id2freshId, fd2FreshFd)) ++
+ extraArgs.map(v => replace(id2freshId.map(p => (p._1.toVariable, p._2.toVariable)), v))).setPosInfo(fi)
}
case n @ NAryOperator(args, recons) => {
val rargs = args.map(a => functionClosure(a, bindedVars, id2freshId, fd2FreshFd))
@@ -114,7 +117,7 @@ object FunctionClosure extends Pass {
val r = functionClosure(t, bindedVars, id2freshId, fd2FreshFd)
recons(r).setType(u.getType)
}
- case m @ MatchExpr(scrut,cses) => { //still needs to handle the new ids introduced by the patterns
+ case m @ MatchExpr(scrut,cses) => {
val scrutRec = functionClosure(scrut, bindedVars, id2freshId, fd2FreshFd)
val csesRec = cses.map{
case SimpleCase(pat, rhs) => {
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 4d3dab3d0f84fa215a588712bfe82e57f63abb51..ae7d8c0e5c90f54afc179b5ee17fbf1ef885db1b 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -1065,6 +1065,10 @@ trait CodeExtraction extends Extractors {
case LetVar(_, _, rest) => getReturnedExpr(rest)
case PBlock(_, rest) => getReturnedExpr(rest)
case IfExpr(_, then, elze) => getReturnedExpr(then) ++ getReturnedExpr(elze)
+ case MatchExpr(_, cses) => cses.flatMap{
+ case SimpleCase(_, rhs) => getReturnedExpr(rhs)
+ case GuardedCase(_, _, rhs) => getReturnedExpr(rhs)
+ }
case _ => Seq(expr)
}
diff --git a/testcases/regression/valid/Nested10.scala b/testcases/regression/valid/Nested10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b3c4f865367ca84a52091e89b655ac6438dc65a2
--- /dev/null
+++ b/testcases/regression/valid/Nested10.scala
@@ -0,0 +1,14 @@
+object Nested10 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = {
+ i + j + n
+ }
+ def rec2(j: Int) = {
+ rec1(j)
+ }
+ rec2(2)
+ } ensuring(i + 4 == _)
+
+}
diff --git a/testcases/regression/valid/Nested11.scala b/testcases/regression/valid/Nested11.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0316fc5f2ba3497691bc48b1d573933ba2cea027
--- /dev/null
+++ b/testcases/regression/valid/Nested11.scala
@@ -0,0 +1,14 @@
+object Nested11 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(j: Int) = b match {
+ case B(b) => i + j + b
+ }
+ rec1(2)
+ } ensuring(i + 5 == _)
+
+}
diff --git a/testcases/regression/valid/Nested12.scala b/testcases/regression/valid/Nested12.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05ac1569f630f1fc905a84f0550cbbaa42047906
--- /dev/null
+++ b/testcases/regression/valid/Nested12.scala
@@ -0,0 +1,17 @@
+object Nested12 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(a: A, j: Int, j2: Int) = a match {
+ case B(b) => i + j + j2 + b
+ }
+ def rec2(a: A, k: Int) = a match {
+ case B(b) => rec1(a, b, k)
+ }
+ rec2(b, 2)
+ } ensuring(i + 8 == _)
+
+}
diff --git a/testcases/regression/valid/Nested13.scala b/testcases/regression/valid/Nested13.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ccb742494564433dffe096210fac07b37a663dfe
--- /dev/null
+++ b/testcases/regression/valid/Nested13.scala
@@ -0,0 +1,21 @@
+object Nested13 {
+
+ abstract class D
+ case class E(e: Int) extends D
+ case class F(d: D, f: Int) extends D
+
+ def foo(a : Int): Int = {
+
+ def rec1(d: D, j: Int): Int = d match {
+ case E(e) => j + e + a
+ case F(dNext, f) => f + rec1(dNext, j)
+ }
+
+ def rec2(d: D, i : Int) : Int = d match {
+ case E(e) => e
+ case F(dNext, f) => rec1(d, i)
+ }
+
+ rec2(F(E(2), 3), 0)
+ } ensuring(a + 5 == _)
+}
diff --git a/testcases/regression/valid/Nested14.scala b/testcases/regression/valid/Nested14.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba
--- /dev/null
+++ b/testcases/regression/valid/Nested14.scala
@@ -0,0 +1,11 @@
+object Nested14 {
+
+ def foo(i: Int): Int = {
+ def rec1(j: Int): Int = {
+ def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
+ rec2(j)
+ }
+ rec1(3)
+ } ensuring(0 == _)
+
+}