From ccdbaa76738e07a2767f1c39669698e0c58c6ca7 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 14 Apr 2016 18:37:38 +0200
Subject: [PATCH] Small fix for required lambda in ensuring
---
src/main/scala/leon/purescala/Path.scala | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index 6bc93410d..3d3f329e7 100644
--- a/src/main/scala/leon/purescala/Path.scala
+++ b/src/main/scala/leon/purescala/Path.scala
@@ -81,7 +81,10 @@ class Path private[purescala](
def wrap(e: Expr) = fold[Expr](e, let, (_, res) => res)(rest)
val req = Require(Constructors.and(cond, wrap(pre)), wrap(body))
- val full = if (post != NoTree(BooleanType)) Ensuring(req, wrap(post)) else req
+ val full = post match {
+ case l @ Lambda(args, body) => Ensuring(req, Lambda(args, wrap(body)).copiedFrom(l))
+ case _ => req
+ }
fold[Expr](full, let, (_, _) => scala.sys.error("Should never happen!"))(outers)
}
--
GitLab