diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 656104b92307f81cf9576fb57d2ecd15a82b7a80..2daf0696c6230c5698fdef1d53010d037382f6c5 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -244,6 +244,11 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
         val (bodyRes, bodyScope, bodyFun) = toFunction(b)
         (bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)), bodyFun)
       }
+      case Choose(ids, b) => {
+        //Recall that Choose cannot mutate variables from the scope
+        val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+        (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)), bodyFun)
+      }
       case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
       case n @ NAryOperator(args, recons) => {
         val (recArgs, scope, fun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..702024e96bb89a6d1fa793e2b9b05663eba7fff7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
@@ -0,0 +1,14 @@
+import leon.Utils._
+
+object Test {
+
+  def test(x: Int): Int = {
+
+    choose((y: Int) => {
+      val z = y + 2
+      z == y
+    })
+
+  } ensuring(_ == x + 2)
+
+}