diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 299e8995a072084bba0adf0a98603e64b1611aac..0a75dfebc5ae78d8147d0f601d61d38e2e0c05e2 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)