From d61ac65510f3dcf3f00dcc2faa8b77c6ea2f2b4f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 14 Oct 2015 19:50:35 +0200
Subject: [PATCH] should still transform the body even without side effects
---
src/main/scala/leon/xlang/ImperativeCodeElimination.scala | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 8726a02a6..1398aee1a 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -254,6 +254,10 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
case LetDef(fd, b) =>
def fdWithoutSideEffects = {
+ fd.body.foreach { bd =>
+ val (fdRes, fdScope, _) = toFunction(bd)
+ fd.body = Some(fdScope(fdRes))
+ }
val (bodyRes, bodyScope, bodyFun) = toFunction(b)
(bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)).copiedFrom(expr), bodyFun)
}
--
GitLab