diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 8d6c9cef987cd53f407683ef647c70d64b584658..9a80528f336ffc7a5f9cf5289d94a8e7933c098d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1064,7 +1064,14 @@ trait CodeExtraction extends ASTExtractors {
               NoTree(toPureScalaType(current.tpe)(dctx, current.pos))
           }
 
-          Ensuring(b, post)
+          val closure = post.getType match {
+            case BooleanType =>
+              val resId = FreshIdentifier("res", BooleanType).setPos(post).setOwner(currentFunDef)
+              Lambda(Seq(LeonValDef(resId)), post).setPos(post)
+            case _ => post
+          }
+
+          Ensuring(b, closure)
 
         case t @ ExHoldsExpression(body) =>
           val resId = FreshIdentifier("holds", BooleanType).setPos(current.pos).setOwner(currentFunDef)
diff --git a/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala b/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8d9c793b5878eda52a0532f53cca0620a378eb09
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/EnsuringBoolean.scala
@@ -0,0 +1,10 @@
+import leon._
+import leon.lang._
+import leon.annotation._
+import scala.language.postfixOps 
+object EnsuringBoolean {
+  def congR(x: BigInt)(implicit mod: BigInt): Unit = {
+    require(mod >= 1);
+    ()
+  } ensuring(false)
+}