From 6562b9f32c5184c387582d44e6a0aec666569298 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 22 Oct 2015 11:32:49 +0200
Subject: [PATCH] keep positions in post conditions
---
src/main/scala/leon/xlang/ImperativeCodeElimination.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 364c6fbb2..7a00cb7f8 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -316,7 +316,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(v.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap +
(res.toVariable -> TupleSelect(newRes.toVariable, 1)),
postBody)
- Lambda(Seq(newRes), newBody)
+ Lambda(Seq(newRes), newBody).setPos(post)
})
val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withFunDef(fd, newFd, modifiedVars))
--
GitLab