diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala index 8726a02a6f5a6b82c1fb6c2f43e6249be8fdd0ce..1398aee1a03451bbcb47e046d1b6a920e22b4811 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) }