From 3e95c2b16ae22fd12f0ba2e4ff72f7c27c82cdd3 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 17 Mar 2015 12:20:14 +0100
Subject: [PATCH] Remove one TODO from XLang
---
src/main/scala/leon/utils/UnitElimination.scala | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index e5672bd51..60f8bc232 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -97,10 +97,8 @@ object UnitElimination extends TransformationPhase {
val (newFd, rest) = if(fd.params.exists(vd => vd.getType == UnitType)) {
val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.returnType, fd.params.filterNot(vd => vd.getType == UnitType), fd.defType).setPos(fd)
freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
- freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
- freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
fun2FreshFun += (fd -> freshFunDef)
- freshFunDef.body = fd.body.map(b => removeUnit(b))
+ freshFunDef.fullBody = removeUnit(fd.fullBody)
val restRec = removeUnit(b)
fun2FreshFun -= fd
(freshFunDef, restRec)
--
GitLab