diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index de75b7a29c0494ba4052aefe9fcb4f974dd128a2..3636fd6e51b8563c27963c3908d906d237b2d772 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -304,6 +304,11 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
           }
         }
 
+      //TODO: handle vars in scope, just like LetDef
+      case ld@Lambda(params, body) =>
+        val (bodyVal, bodyScope, bodyFun) = toFunction(body)
+        (Lambda(params, bodyScope(bodyVal)).copiedFrom(ld), (e: Expr) => e, Map())
+
       case c @ Choose(b) =>
         //Recall that Choose cannot mutate variables from the scope
         (c, (b2: Expr) => b2, Map())
diff --git a/src/test/resources/regression/verification/xlang/valid/Lambda1.scala b/src/test/resources/regression/verification/xlang/valid/Lambda1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b228f96f7c861d0b1fb020c7f65d4e84ea8b7ab9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Lambda1.scala
@@ -0,0 +1,13 @@
+object Lambda1 {
+
+  def test(): Int = {
+    val x = 2
+    val cl = ((y: Int) => {
+      var z = y
+      z = z + x
+      z
+    })
+    cl(4)
+  } ensuring(_ == 6)
+
+}