diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 857351286f787afec22e082ee3ec59e8fc4d4a3b..dbb08ef3320eb77cc84365a0c271be37f9e8d057 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -63,19 +63,12 @@ type extension = {
   short_printer: extension_printer ;
 }
 
-let default_printer name printer fmt = function
-  | Ext_id i ->
-    Format.fprintf fmt "@[<hov 2>%s %d;@]" name i
-  | Ext_terms ts ->
-    Format.fprintf fmt "@[<hov 2>%s %a;@]" name
-    (Pretty_utils.pp_list ~sep:",@ " printer#term) ts
-  | Ext_preds ps ->
-    Format.fprintf fmt "@[<hov 2>%s %a;@]" name
-    (Pretty_utils.pp_list ~sep:",@ " printer#predicate) ps
-  | Ext_annot (id,an) ->
-    Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" name id
-      (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
-            printer#extended) an
+let default_printer printer fmt = function
+  | Ext_id i -> Format.fprintf fmt "%d" i
+  | Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
+  | Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
+  | Ext_annot (_,an) -> Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+                                 printer#extended fmt an
 
 let default_short_printer name printer fmt = function
   | Ext_id _ | Ext_terms _ | Ext_preds _ -> Format.fprintf fmt "%s" name
@@ -87,7 +80,7 @@ let make
     ?(preprocessor=Extlib.id)
     typer
     ?(visitor=fun _ _ -> Cil.DoChildren)
-    ?(printer=default_printer name)
+    ?(printer=default_printer)
     ?(short_printer=default_short_printer name)
     status : extension_standard*extension_commun =
   { preprocessor; typer; status},{ category; visitor; printer; short_printer }
@@ -97,7 +90,7 @@ let make_block
     ?(preprocessor=Extlib.id)
     typer
     ?(visitor=fun _ _ -> Cil.DoChildren)
-    ?(printer=default_printer name)
+    ?(printer=default_printer)
     ?(short_printer=default_short_printer name)
     status : extension_block*extension_commun =
   { preprocessor; typer; status},{ category; visitor; printer; short_printer }
@@ -201,8 +194,12 @@ module Extensions = struct
   let visit name = (find_commun name).visitor
 
   let print name printer fmt kind =
-    let pp = (find_commun name).printer in
-    pp printer fmt kind
+    let pp = (find_commun name).printer printer in
+    match kind with
+    | Ext_annot (id,_) ->
+      Format.fprintf fmt "@[<v 2>@[%s %s {@]@\n%a}@]" name id pp kind
+    | _ ->
+      Format.fprintf fmt "@[<hov 2>%s %a;@]" name pp kind
 
   let short_print name printer fmt kind =
     let pp = (find_commun name).short_printer in
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 71fcdbdc871433955ef45aa232fd62b5f0c3b93b..af1f9f6510af20f330150938ce0703849e464a3c 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -40,7 +40,7 @@ let print_bar prt fmt ext =
     let l = Bar_table.find idx in
     Pretty_utils.pp_list
       ~pre:"@[<hov 2>" ~sep:",@ " ~suf:"@]" prt#predicate fmt l
-  | Ext_preds _ | Ext_terms _ ->
+  | Ext_preds _ | Ext_terms _ | Ext_annot _->
     Kernel.fatal "bar extension should have ids as arguments"
 
 let visit_bar vis ext =
@@ -56,7 +56,7 @@ let visit_bar vis ext =
       Bar_table.replace idx l';
       Cil.SkipChildren
     end
-  | Ext_terms _ | Ext_preds _ ->
+  | Ext_terms _ | Ext_preds _ | Ext_annot _ ->
       Kernel.fatal "bar extension should have ids as arguments"
 
 let type_baz typing_context _loc l =