diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index f1b5ab00c66af69aa7d722dccca1787ab8e07fed..2b8c620ea6b01e18ec5c712bce14e2b39c4ee70f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1180,6 +1180,9 @@ class cil_printer () = object (self)
 
   method annotated_stmt (next: stmt) fmt (s: stmt) =
     pp_open_hvbox fmt 0;
+    if Kernel.is_debug_key_enabled Kernel.dkey_print_sid then begin
+      Format.fprintf fmt "/* sid:%d */@\n" s.sid;
+    end;
     (* print the statement. *)
     if Cil.is_skip s.skind && not s.ghost && s.sattr = [] then begin
       if verbose || s.labels <> [] then begin