Extracting loop invariant

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)

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(