diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1c6dc98bce5eb1138c90a0408724a098b5c99a19
--- /dev/null
+++ b/mytest/Bubble.scala
@@ -0,0 +1,33 @@
+import leon.Utils._
+
+object Bubble {
+
+  def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = {
+    require(isArray(a, size))
+    var i = size - 1
+    var j = 0
+    var sortedArray = a
+    (while(i > 0) {
+      j = 0
+      (while(j < i) {
+        if(a(j) > a(j+1)) {
+          val tmp = sortedArray(j)
+          sortedArray = sortedArray.updated(j, a(j+1))
+          sortedArray = sortedArray.updated(j+1, tmp)
+        }
+        j = j + 1
+      }) invariant(isArray(sortedArray, size) && j >= 0 && j <= i && i < size && i >= 0)
+      i = i - 1
+    }) invariant(isArray(sortedArray, size) && i >= 0 && i < size)
+    sortedArray
+  }
+
+
+  def isArray(a: Map[Int, Int], size: Int): Boolean = {
+    def rec(i: Int): Boolean = if(i >= size) true else {
+      if(a.isDefinedAt(i)) rec(i+1) else false
+    }
+    size > 0 && rec(0)
+  }
+
+}
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 6ec1a95b6c86189e2f51aee02ab6b4d3b2272d17..9598f3901d9b358b06de1082bf0c552d8f7715dd 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -21,7 +21,12 @@ object FunctionClosure extends Pass {
   }
 
   private def functionClosure(expr: Expr, bindedVars: Set[Identifier]): Expr = expr match {
-    case l @ LetDef(fd@FunDef(id, rt, varDecl, Some(funBody), _, _), rest) => {
+    case l @ LetDef(fd, rest) => {
+      val id = fd.id
+      val rt = fd.returnType
+      val varDecl = fd.args
+      val funBody = fd.getBody
+      val previousEnclosingPreconditions = enclosingPreconditions
       enclosingPreconditions = fd.precondition match {
         case Some(pre) => pre :: enclosingPreconditions
         case None => enclosingPreconditions
@@ -37,9 +42,10 @@ object FunctionClosure extends Pass {
       val newVarDecls = varDecl ++ extraVarDecls
       val newFunId = FreshIdentifier(id.name)
       val newFunDef = new FunDef(newFunId, rt, newVarDecls)
+      enclosingPreconditions = enclosingPreconditions.map(pre => replace(freshVarsExpr, pre)) //introduce the new variables name for the list of preconditions
       newFunDef.precondition = enclosingPreconditions match {
         case List() => None
-        case precs => Some(replace(freshVarsExpr, And(precs)))
+        case precs => Some(And(precs))
       }
       newFunDef.postcondition = fd.postcondition.map(expr => replace(freshVarsExpr, expr))
       def substFunInvocInDef(expr: Expr): Option[Expr] = expr match {
@@ -54,10 +60,7 @@ object FunctionClosure extends Pass {
         case _ => None
       }
       //need to remove the enclosing precondition before considering the rest
-      enclosingPreconditions = fd.precondition match {
-        case Some(_) => enclosingPreconditions.tail
-        case None => enclosingPreconditions
-      }
+      enclosingPreconditions = previousEnclosingPreconditions
       val recRest = functionClosure(rest, bindedVars)
       val recRest2 = searchAndReplaceDFS(substFunInvocInRest)(recRest)
       LetDef(newFunDef, recRest2).setType(l.getType)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 754ecdef43dc0eed839817791b64560b1da638a0..6ea8372e362ec7db7ddbb02f2b969271c0fb58e8 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -427,7 +427,9 @@ trait CodeExtraction extends Extractors {
             case None => UnitLiteral
           }
           handleRest = false
-          Let(newID, valTree, restTree)
+          val res = Let(newID, valTree, restTree)
+          println(res + " with type: " + res.getType + " and restree type: " + restTree.getType)
+          res
         }
         case dd@ExFunctionDef(n, p, t, b) => {
           val funDef = extractFunSig(n, p, t).setPosInfo(dd.pos.line, dd.pos.column)
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 2672f2d02dcd01bd3f379ae8e046eded78619b37..10410e0e5c646d39377dd2113cff13617bf8f8e6 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -17,7 +17,12 @@ object Trees {
     self: Expr =>
   }
 
-  case class Block(exprs: Seq[Expr], last: Expr) extends Expr
+  case class Block(exprs: Seq[Expr], last: Expr) extends Expr {
+    val t = last.getType
+    if(t != Untyped)
+      setType(t)
+  }
+
   case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType {
     val fixedType = UnitType
   }
@@ -500,8 +505,10 @@ object Trees {
             l
         }
         case l @ LetDef(fd, b) => {
-          //TODO, not sure
-          fd.body = Some(rec(fd.getBody))
+          //TODO, not sure, see comment for the next LetDef
+          fd.body = fd.body.map(rec(_))
+          fd.precondition = fd.precondition.map(rec(_))
+          fd.postcondition = fd.postcondition.map(rec(_))
           LetDef(fd, rec(b)).setType(l.getType)
         }
         case n @ NAryOperator(args, recons) => {
@@ -588,8 +595,10 @@ object Trees {
         })
       }
       case l @ LetDef(fd,b) => {
-        //TODO: Not sure
-        fd.body = Some(rec(fd.getBody))
+        //TODO: Not sure: I actually need the replace to occurs even in the pre/post condition, hope this is correct
+        fd.body = fd.body.map(rec(_))
+        fd.precondition = fd.precondition.map(rec(_))
+        fd.postcondition = fd.postcondition.map(rec(_))
         val rl = LetDef(fd, rec(b)).setType(l.getType)
         applySubst(rl)
       }