diff --git a/src/main/scala/leon/Utils.scala b/src/main/scala/leon/Utils.scala
index 6d7f019ce669a9e81f7da0380048d0071d6713bc..9ed8ef400ea0f143af078149c0d3b3034394c3a4 100644
--- a/src/main/scala/leon/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -9,4 +9,10 @@ object Utils {
   }
 
   implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
+
+
+  object InvariantFunction {
+    def invariant(x: Boolean): Unit = ()
+  }
+  implicit def while2Invariant(u: Unit) = InvariantFunction
 }