Do not accept letdef in precondition and postcondition

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))

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