diff --git a/library/leon/lang/StaticChecks.scala b/library/leon/lang/StaticChecks.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e53f2def0bac9146a4a2ee615224e321b7b0ee6d
--- /dev/null
+++ b/library/leon/lang/StaticChecks.scala
@@ -0,0 +1,14 @@
+package leon.lang
+
+import leon.annotation._
+import scala.language.implicitConversions
+
+object StaticChecks {
+
+  case class Ensuring[A](x: A) {
+    def ensuring(cond: (A) => Boolean): A = x
+  }
+
+  implicit def any2Ensuring[A](x: A): Ensuring[A] = Ensuring(x)
+
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 02a58ad2930ff51e80d19f22b41029f30d3f999c..5fb96861de6c6eeab14de3954bd2e05bc9a17612 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -171,6 +171,8 @@ trait ASTExtractors {
       def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
         case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
           => Some((body, contract))
+        case Apply(Select(Apply(TypeApply(ExSelected("leon", "lang", "StaticChecks", "any2Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil)
+          => Some((body, contract))
         case _ => None
       }
     }