From 74c2cfefbe0c1e789436e9beaf4bf839c657f538 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 23 Apr 2013 18:11:10 +0200
Subject: [PATCH] Restore positions of Chooses trated within
ImperativeCodeElimination
---
src/main/scala/leon/xlang/ImperativeCodeElimination.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 2daf0696c..aeda95f09 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) => {
--
GitLab