From b2c422f56971e2012b54a71c1d931de88cd207a5 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 22 Apr 2016 18:26:48 +0200
Subject: [PATCH] while loops with distinguishable names
---
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 3636fd6e5..6326ff8e4 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -129,7 +129,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
case wh@While(cond, body) =>
- val whileFunDef = new FunDef(parent.id.freshen, Nil, Nil, UnitType).setPos(wh)
+ val whileFunDef = new FunDef(parent.id.duplicate(name = (parent.id.name + "While")), Nil, Nil, UnitType).setPos(wh)
whileFunDef.addFlag(IsLoop(parent))
whileFunDef.body = Some(
IfExpr(cond,
--
GitLab