diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 2daf0696c6230c5698fdef1d53010d037382f6c5..aeda95f09de30c6b001f2f8f827ae60d3bfa3d1e 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -244,10 +244,10 @@ 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) => {
+      case c @ 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)
+        (bodyRes, (b2: Expr) => Choose(ids, bodyScope(b2)).setPosInfo(c), bodyFun)
       }
       case n @ NAryOperator(Seq(), recons) => (n, (body: Expr) => body, Map())
       case n @ NAryOperator(args, recons) => {