From 6d72a6349acc23b68592a6e8f37b9481dd2a273d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Oct 2015 18:05:44 +0200
Subject: [PATCH] Wrap non-lambda ensuring into a lambda
---
.../scala/leon/frontends/scalac/CodeExtraction.scala | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 299e8995a..0a75dfebc 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -984,11 +984,14 @@ trait CodeExtraction extends ASTExtractors {
val b = extractTreeOrNoTree(body)
- val closure = post.getType match {
- case BooleanType =>
+ val closure = post match {
+ case IsTyped(_, BooleanType) =>
val resId = FreshIdentifier("res", b.getType).setPos(post)
Lambda(Seq(LeonValDef(resId)), post).setPos(post)
- case _ => post
+ case l: Lambda => l
+ case other =>
+ val resId = FreshIdentifier("res", b.getType).setPos(post)
+ Lambda(Seq(LeonValDef(resId)), application(other, Seq(Variable(resId)))).setPos(post)
}
Ensuring(b, closure)
--
GitLab