diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c96a5e1b00a00ed4599dbf920af667d05e494a74..cd8d3806d7e91d1f1fc4bd7d8213b8bb832abb99 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1442,15 +1442,15 @@ class cil_printer () = object (self)
         directive (fst l).Filepath.pos_lnum filename
 
   (* Print a recovered while condition from Loop *)
-  method pp_while fmt cond =
+  method pp_while_head fmt cond =
     fprintf fmt "%a (%a)"
       self#pp_keyword "while"
       self#exp cond
 
-  method private stacked_while ~stmt ~cond fmt =
+  method private pp_while_head_stacked ~stmt ~cond fmt =
     begin
       Stack.push stmt current_stmt;
-      self#pp_while fmt cond;
+      self#pp_while_head fmt cond;
       ignore (Stack.pop current_stmt);
     end
 
@@ -1642,7 +1642,7 @@ class cil_printer () = object (self)
           in
           Format.fprintf fmt "%a@[<v 2>%t %t%a@]"
             (fun fmt -> self#line_directive fmt) l
-            (self#stacked_while ~stmt ~cond)
+            (self#pp_while_head_stacked ~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 f9236745782d9560d031377af9c8b881033b5a8d..230e0bce02e2d3d40acd5546890ccc138b014ec0 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -312,11 +312,11 @@ class type extensible_printer_type = object
   (** {3 Modifying pretty-printer behavior}                              *)
   (* ******************************************************************* *)
 
-  method pp_while: Format.formatter -> exp -> unit
-  (** Prints the recovered [while (cond)] exit condition of a loop. The current
-      stmt is expected to be positionned to the original AST statement
-      containing the breaking condition (which is not printed at all). *)
-
+  method pp_while_head: Format.formatter -> exp -> unit
+  (** Prints the recovered [while (cond)] exit condition of a loop. Note: this
+      method will be called in a context where 'current_stmt' is tied to the
+      original AST conditional statement that exits the loop, as expected. *)
+    
   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 f392f73483facfb2114ddd315b188053f829d12e..867ccc778358e87daa5b5413c9b039b9c83cad4c 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -582,12 +582,12 @@ struct
             pp_by_kf fmt ips_all_kfs
       | _ -> ()
 
-    method! pp_while fmt cond =
+    method! pp_while_head fmt cond =
       let kf = Option.get self#current_kf in
       let stmt = Option.get self#current_stmt in
       Format.fprintf fmt "@{<%s>%a@}"
         (Tag.create (PStmtStart(kf,stmt)))
-        super#pp_while cond
+        super#pp_while_head cond
 
     method! next_stmt next fmt current =
       if Tag.unfold current