diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 8f26df8f410e614dc58ce83d88737d40fa42d50f..7b340a12ae62d51c2fb1a3ce0e3aa6f3044d5593 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -155,7 +155,7 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
           val whileFunDef = new FunDef(FreshIdentifier(parent.id.name), Nil, whileFunReturnType, whileFunValDefs,DefType.MethodDef).setPos(wh)
           wasLoop += whileFunDef
           
-          val whileFunCond = condRes
+          val whileFunCond = condScope(condRes)
           val whileFunRecursiveCall = replaceNames(condFun,
             bodyScope(FunctionInvocation(whileFunDef.typed, modifiedVars.map(id => condBodyFun(id).toVariable)).setPos(wh)))
           val whileFunBaseCase =
diff --git a/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala b/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b57fc9d8ba3aa2e1f45a38116daf8a5ac7ba86c9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/WhileConditionSubexpression.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+import leon.lang._
+
+object WhileConditionSubexpression {
+
+  def test(x: Int): Boolean = {
+    var b = false
+    var i = 0
+    while(!b && i < 10) {
+      if(i == x)
+        b = true
+      i += 1
+    }
+    b
+  } ensuring(res => res || (x != 0 && x != 1 && x != 2))
+
+}