Function closure makes sure that all ids updated

src/main/scala/leon/purescala/DefinitionTransformer.scala

@@ -45,11 +45,6 @@ class DefinitionTransformer(
               idMap += id -> nid
               nid
           })
-        case LetDef(fds, body) =>
-          val rFds = fds map transform
-          val rBody = transform(body)
-          LetDef(rFds, rBody).copiedFrom(e)
-          
         case _ => super.transform(e)
       }
     }

src/main/scala/leon/purescala/FunctionClosure.scala

@@ -180,6 +180,9 @@ object FunctionClosure extends TransformationPhase {
       case _ => None
     }(instBody)
 
+    //HACK to make sure substitution happened even in nested fundef
+    newFd.fullBody = replaceFromIDs(freeMap.map(p => (p._1, p._2.toVariable)), newFd.fullBody)
+
     FunSubst(newFd, freeMap, tparamsMap.map{ case (from, to) => from.tp -> to})
   }
 

src/main/scala/leon/purescala/TreeTransformer.scala

@@ -38,6 +38,10 @@ trait TreeTransformer {
     case LetVar(a, expr, body) =>
       val newA = transform(a)
       LetVar(newA, transform(expr), transform(body)(bindings + (a -> newA))).copiedFrom(e)
+    case LetDef(fds, body) =>
+      val rFds = fds map transform
+      val rBody = transform(body)
+      LetDef(rFds, rBody).copiedFrom(e)
     case CaseClass(cct, args) =>
       CaseClass(transform(cct).asInstanceOf[CaseClassType], args map transform).copiedFrom(e)
     case CaseClassSelector(cct, caseClass, selector) =>

src/test/resources/regression/verification/purescala/valid/Nested18.scala

+object Nested18 {
+
+  def test(a: BigInt): BigInt = {
+    require(a > 0)
+    def f(b: BigInt): BigInt = {
+      def g(c: BigInt): BigInt = {
+        require(a > 0)
+        c
+      }
+      g(b)
+    }
+    f(12)
+  }
+
+}

src/test/scala/leon/unit/purescala/FunctionClosureSuite.scala

@@ -97,6 +97,38 @@ class FunctionClosureSuite extends FunSuite with helpers.ExpressionsDSL {
         fail("Unexpected fun def: " + cfd)
       }
     })
+
+
+    val deeplyNested2 = new FunDef(FreshIdentifier("deeplyNested"), Seq(), Seq(ValDef(z.id)), IntegerType)
+    deeplyNested2.body = Some(Require(GreaterEquals(x, bi(0)), z))
+
+    val nested2 = new FunDef(FreshIdentifier("nested"), Seq(), Seq(ValDef(y.id)), IntegerType)
+    nested2.body = Some(LetDef(Seq(deeplyNested2), FunctionInvocation(deeplyNested2.typed, Seq(y))))
+
+    val fd2 = new FunDef(FreshIdentifier("f"), Seq(), Seq(ValDef(x.id)), IntegerType)
+    fd2.body = Some(Require(GreaterEquals(x, bi(0)),
+                    LetDef(Seq(nested2), FunctionInvocation(nested2.typed, Seq(x)))))
+
+    val cfds2 = FunctionClosure.close(fd2)
+    assert(cfds2.size === 3)
+
+    cfds2.foreach(cfd => {
+      if(cfd.id.name == "f") {
+        assert(cfd.returnType === fd2.returnType)
+        assert(cfd.params.size === fd2.params.size)
+        assert(freeVars(cfd).isEmpty)
+      } else if(cfd.id.name == "nested") {
+        assert(cfd.returnType === nested2.returnType)
+        assert(cfd.params.size === 2)
+        assert(freeVars(cfd).isEmpty)
+      } else if(cfd.id.name == "deeplyNested") {
+        assert(cfd.returnType === deeplyNested2.returnType)
+        assert(cfd.params.size === 2)
+        assert(freeVars(cfd).isEmpty)
+      } else {
+        fail("Unexpected fun def: " + cfd)
+      }
+    })
   }
 
   private def freeVars(fd: FunDef): Set[Identifier] = variablesOf(fd.fullBody) -- fd.paramIds