From 86f0b2695e3eb4a4d5292c7dc30c13fa4665062c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 8 Mar 2013 16:27:51 +0100
Subject: [PATCH] Remove hack
---
src/main/scala/leon/purescala/TreeOps.scala | 11 -----------
1 file changed, 11 deletions(-)
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index b0516a56f..9d7369d99 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1191,17 +1191,6 @@ object TreeOps {
protected def register(cond: Expr, path: C): C
protected def rec(e: Expr, path: C): Expr = e match {
- case Let(i, e @ FunctionInvocation(fd, callArgs), b) if fd.hasPostcondition =>
- val argsMap = fd.args.map(vd => Variable(vd.id)) zip callArgs
-
- val newPost = TreeOps.replace(Map(ResultVariable() -> Variable(i)) ++ argsMap, fd.postcondition.get)
-
- val pred = newPost
-
- val se = rec(e, path)
- val sb = rec(b, register(pred, path))
- Let(i, se, sb)
-
case Let(i, e, b) =>
val se = rec(e, path)
val sb = rec(b, register(Equals(Variable(i), se), path))
--
GitLab