diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index 3cc81b703e96179337090ec69b29a1effbcf738b..d3cd29907c5cd8c30fb574d06ddd1682e5bfa59a 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -225,8 +225,13 @@ object ImperativeCodeElimination extends Pass {
       }
       case LetDef(fd, b) => {
         //Recall that here the nested function should not access mutable variables from an outside scope
+        val newFd = if(!fd.hasImplementation) fd else {
+          val (fdRes, fdScope, fdFun) = toFunction(fd.getBody)
+          fd.body = Some(fdScope(fdRes))
+          fd
+        }
         val (bodyRes, bodyScope, bodyFun) = toFunction(b)
-        (bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)), bodyFun)
+        (bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)), bodyFun)
       }
       case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
       case n @ NAryOperator(args, recons) => {
diff --git a/testcases/regression/valid/IfExpr3.scala b/testcases/regression/valid/IfExpr3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86d4e494a7ce8fd22024020bb9580b393af8377a
--- /dev/null
+++ b/testcases/regression/valid/IfExpr3.scala
@@ -0,0 +1,19 @@
+object IfExpr1 {
+
+  def foo(a: Int): Int = {
+
+    if(a > 0) {
+      var a = 1
+      var b = 2
+      a = 3
+      a + b
+    } else {
+      5
+      //var a = 3
+      //var b = 1
+      //b = b + 1
+      //a + b
+    }
+  } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/IfExpr4.scala b/testcases/regression/valid/IfExpr4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..94b99fde39e6f7e10b1c898548d60592023ffbd6
--- /dev/null
+++ b/testcases/regression/valid/IfExpr4.scala
@@ -0,0 +1,18 @@
+object IfExpr4 {
+
+  def foo(a: Int): Int = {
+
+    if(a > 0) {
+      var a = 1
+      var b = 2
+      a = 3
+      a + b
+    } else {
+      var a = 3
+      var b = 1
+      b = b + 1
+      a + b
+    }
+  } ensuring(_ == 5)
+
+}
diff --git a/testcases/regression/valid/NestedVar.scala b/testcases/regression/valid/NestedVar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a26b7312b2f5f85509c6e55cc706fb29845202b1
--- /dev/null
+++ b/testcases/regression/valid/NestedVar.scala
@@ -0,0 +1,17 @@
+object NestedVar {
+
+  def foo(): Int = {
+    val a = 3
+    def rec(x: Int): Int = {
+      var b = 3
+      var c = 3
+      if(x > 0)
+        b = 2
+      else
+        c = 2
+      c+b
+    }
+    rec(a)
+  } ensuring(_ == 5)
+
+}