diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index dc287b62dd95d30d211df1dc8eaf49599e466b93..ec7236d50b3458edccc84fdd7551f0300f96cf02 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -110,7 +110,18 @@ object PrettyPrinter {
       sb
     }
     case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
-    case While(cond, body) => {
+    case wh@While(cond, body) => {
+      wh.invariant match {
+        case Some(inv) => {
+          sb.append("\n")
+          ind(sb, lvl)
+          sb.append("@invariant: ")
+          pp(inv, sb, lvl)
+          sb.append("\n")
+          ind(sb, lvl)
+        }
+        case None =>
+      }
       sb.append("while(")
       pp(cond, sb, lvl)
       sb.append(")\n")