diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index a180b1f168f1f0b304ded85491f2a4e8bdd4f31b..d9426510ee76f9703514df4219cff8761db26995 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -72,14 +72,11 @@ object FunctionClosure extends Pass {
       val recBody = freshBody.map(b =>
                       functionClosure(b, bindedVars ++ newVarDecls.map(_.id))
                     ).map(b => searchAndReplaceDFS(substFunInvocInDef)(b))
-      val recPostcondition = freshPostcondition.map(expr =>
-                               functionClosure(expr, bindedVars ++ newVarDecls.map(_.id))
-                             ).map(expr => searchAndReplaceDFS(substFunInvocInDef)(expr))
       pathConstraints = oldPathConstraints
 
       newFunDef.precondition = recPrecondition
       newFunDef.body = recBody
-      newFunDef.postcondition = recPostcondition
+      newFunDef.postcondition = freshPostcondition
 
       def substFunInvocInRest(expr: Expr): Option[Expr] = expr match {
         case fi@FunctionInvocation(fd, args) if fd.id == id => Some(FunctionInvocation(newFunDef, args ++ capturedVarsWithConstraints.map(_.toVariable)).setPosInfo(fi))
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 32e600e957dc07934216c2dbd1bee619705a23de..e54690c36b732ae3b3b3e3924d1f54d8b3fc945a 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -290,6 +290,11 @@ trait CodeExtraction extends Extractors {
           unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
           throw ImpureCodeEncounteredException(realBody)
         })
+      ensCont.map(e => 
+        if(containsLetDef(e)) {
+          unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+          throw ImpureCodeEncounteredException(realBody)
+        })
       funDef.body = bodyAttempt
       funDef.precondition = reqCont
       funDef.postcondition = ensCont
@@ -440,6 +445,11 @@ trait CodeExtraction extends Extractors {
           unit.error(realBody.pos, "Function precondtion should not contain nested function definition")
           throw ImpureCodeEncounteredException(realBody)
         })
+      ensCont.map(e => 
+        if(containsLetDef(e)) {
+          unit.error(realBody.pos, "Function postcondition should not contain nested function definition")
+          throw ImpureCodeEncounteredException(realBody)
+        })
       funDef.body = bodyAttempt
       funDef.precondition = reqCont
       funDef.postcondition = ensCont