diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a7ab50d30010d65852dc2b63977a1ee051a7f7e6..179949f14fa62ce0b53d03ffa3805442ec6124c3 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1441,6 +1441,16 @@ class cil_printer () = object (self)
       fprintf fmt "@[@<0>\n@<0>%s@<0> @<0>%d@<0> @<0>%s@]@\n"
         directive (fst l).Filepath.pos_lnum filename
 
+  (* Print a recovered while condition from Loop *)
+  method pp_while ~stmt ~cond fmt =
+    begin
+      Stack.push stmt current_stmt;
+      fprintf fmt "%a (%a)"
+        self#pp_keyword "while"
+        self#exp cond ;
+      ignore (Stack.pop current_stmt);
+    end
+
   method stmtkind sattr (next: stmt) fmt = function
     | UnspecifiedSequence seq ->
       let ctxt =
@@ -1601,7 +1611,7 @@ class cil_printer () = object (self)
               when self#may_be_skipped h-> skipEmpty rest
             | x -> x
           in
-          let term, bodystmts =
+          let stmt, cond, bodystmts =
             (* Bill McCloskey: Do not remove the If if it has labels *)
             match skipEmpty b.bstmts with
             | { skind = If(e,tb,fb,_) } as to_skip :: rest
@@ -1609,18 +1619,17 @@ class cil_printer () = object (self)
                 && self#may_be_skipped to_skip ->
               (match skipEmpty tb.bstmts, skipEmpty fb.bstmts with
                | [], [ { skind = Break _ } as s ] when self#may_be_skipped s ->
-                 e, rest
+                 to_skip, e, rest
                | [], [ { skind = Goto(sref, _) } as s ]
                  when self#may_be_skipped s
                    && Cil_datatype.Stmt.equal !sref next ->
-                 e, rest
+                 to_skip, e, rest
                | [ { skind = Break _ } as s ], [] when self#may_be_skipped s ->
-                 Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
+                 to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
                | [ { skind = Goto(sref, _) } as s ], []
                  when self#may_be_skipped s
                    && Cil_datatype.Stmt.equal !sref next ->
-                 Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
-
+                 to_skip, Cil.dummy_exp (UnOp(LNot, e, Cil.intType)), rest
                | _ -> raise Not_found)
             | _ -> raise Not_found
           in
@@ -1628,10 +1637,9 @@ class cil_printer () = object (self)
               [{ skind=Block b} as s ] when self#may_be_skipped s -> b
             | _ -> { b with bstmts = bodystmts }
           in
-          Format.fprintf fmt "%a@[<v 2>%a (%a) %t%a@]"
+          Format.fprintf fmt "%a@[<v 2>%t %t%a@]"
             (fun fmt -> self#line_directive fmt) l
-            self#pp_keyword "while"
-            self#exp term
+            (self#pp_while ~stmt ~cond)
             pp_sattr
             (self#unboxed_block Other) b;
         with Not_found ->
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index c438c2a9661f9434782f564750c1397244e27aac..6efc412d05fc13f7ed5f7bb36b5abadc3567ce14 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -311,6 +311,12 @@ class type extensible_printer_type = object
   (* ******************************************************************* *)
   (** {3 Modifying pretty-printer behavior}                              *)
   (* ******************************************************************* *)
+
+  method pp_while: stmt:stmt -> cond:exp -> Format.formatter -> unit
+  (** Prints the recovered [while (cond)] condition of a loop. The [stmt]
+      parameter is the original AST statement containing the braking condition,
+      which is no more printed. *)
+
   method pp_keyword: Format.formatter -> string -> unit
   (** All C99 keywords except types "char", "int", "long", "signed",
       "short", "unsigned", "void" and "_XXX" (like "_Bool") **)
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 9f5fe65f343b8cfb6197444b90ecbc7ad77bce6a..6684aa01fc592cf9b165b1fe258fcd8c704e7dbc 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -582,6 +582,10 @@ struct
             pp_by_kf fmt ips_all_kfs
       | _ -> ()
 
+    method! pp_while ~stmt ~cond fmt =
+      Format.fprintf fmt "@{<%s>%t@}"
+        (Tag.create (PStmt(Option.get self#current_kf,stmt)))
+        (super#pp_while ~stmt ~cond)
 
     method! next_stmt next fmt current =
       if Tag.unfold current