diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 9f740b8ff7b36258410780af2fb3b57d142a9f88..754ecdef43dc0eed839817791b64560b1da638a0 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -466,6 +466,14 @@ trait CodeExtraction extends Extractors {
           val bodyTree = rec(body)
           While(condTree, bodyTree)
         }
+        case ExWhileWithInvariant(cond, body, inv) => {
+          val condTree = rec(cond)
+          val bodyTree = rec(body)
+          val invTree = rec(inv)
+          val w = While(condTree, bodyTree)
+          w.invariant = Some(invTree)
+          w
+        }
 
         case ExInt32Literal(v) => IntLiteral(v).setType(Int32Type)
         case ExBooleanLiteral(v) => BooleanLiteral(v).setType(BooleanType)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index 54a5fb7f02c4ddd0d56ee371deddd0700894c660..4bd9f9bf3bb34940a0bf0ea552a89df60b177ec3 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -190,6 +190,16 @@ trait Extractors {
         case _ => None
       }
     }
+    object ExWhileWithInvariant {
+      def unapply(tree: Apply): Option[(Tree, Tree, Tree)] = tree match {
+        case Apply(
+          Select(
+            Apply(while2invariant, List(ExWhile(cond, body))),
+            invariantSym),
+          List(invariant)) if invariantSym.toString == "invariant" => Some((cond, body, invariant))
+        case _ => None
+      }
+    }
     object ExTuple {
       def unapply(tree: Apply): Option[(Seq[Type], Seq[Tree])] = tree match {
         case Apply(