From 179622e24fec9db5e1cfa6f8328d260cf313c89d Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Mon, 7 Mar 2016 14:14:49 +0100
Subject: [PATCH] do not throw away function calls in block desugar
---
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 6b7f7cc6e..506cb86ce 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -155,7 +155,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
val (rVal, rScope, rFun) = toFunction(e)
val scope = (body: Expr) => {
rVal match {
- case FunctionInvocation(tfd, args) if tfd.hasPrecondition =>
+ case FunctionInvocation(tfd, args) =>
rScope(replaceNames(rFun, Let(FreshIdentifier("tmp", tfd.returnType), rVal, accScope(body))))
case _ =>
rScope(replaceNames(rFun, accScope(body)))
--
GitLab