diff --git a/src/main/scala/leon/purescala/Path.scala b/src/main/scala/leon/purescala/Path.scala
index 6bc93410dfee77e050050b70db88d934d70b8f06..3d3f329e7c5abaf7b491ae5b7037497eb02558b3 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)
   }