xlang does not lift code outside of lambdas

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

src/test/resources/regression/verification/xlang/valid/Lambda1.scala

+object Lambda1 {
+
+  def test(): Int = {
+    val x = 2
+    val cl = ((y: Int) => {
+      var z = y
+      z = z + x
+      z
+    })
+    cl(4)
+  } ensuring(_ == 6)
+
+}