diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 18cc9a2e3253c7c04a7d2be4184548a6bb926433..27ac25d6e97bbb1a21983b92b35df25fb2680c68 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -119,7 +119,8 @@ type identified_extended = {
 
 and identified_axiomatic = {
   iax_name : string;
-  iax_props : identified_property list
+  iax_props : identified_property list;
+  iax_attrs : attributes;
 }
 
 and identified_lemma = {
@@ -849,10 +850,11 @@ let rec pretty_debug fmt = function
       Cil_types_debug.pp_toplevel_predicate il_pred
       Cil_types_debug.pp_attributes il_attrs
       Cil_types_debug.pp_location il_loc
-  | IPAxiomatic {iax_name; iax_props} ->
-    Format.fprintf fmt "IPAxiomatic(%a,%a)"
+  | IPAxiomatic {iax_name; iax_props; iax_attrs} ->
+    Format.fprintf fmt "IPAxiomatic(%a,%a,%a)"
       Cil_types_debug.pp_string iax_name
       (Cil_types_debug.pp_list pretty_debug) iax_props
+      Cil_types_debug.pp_attributes iax_attrs
   | IPLemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} ->
     Format.fprintf fmt "IPLemma(%a,%a,%a,%a,%a,%a)"
       Cil_types_debug.pp_string il_name
@@ -1549,9 +1551,9 @@ let ip_of_code_annot_single kf stmt ca = match ip_of_code_annot kf stmt ca with
 let ip_of_global_annotation a =
   let once = true in
   let rec aux acc = function
-    | Daxiomatic(iax_name, l, _, _) ->
+    | Daxiomatic(iax_name, l, iax_attrs, _) ->
       let iax_props = List.fold_left aux [] l in
-      IPAxiomatic {iax_name; iax_props} :: (iax_props @ acc)
+      IPAxiomatic {iax_name; iax_props; iax_attrs} :: (iax_props @ acc)
     | Dlemma(il_name, true, il_labels, il_args, il_pred, il_attrs, il_loc) ->
       ip_axiom {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} :: acc
     | Dlemma(il_name, false, il_labels, il_args, il_pred, il_attrs, il_loc) ->
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index a5eeab817695c32c2b5d873fe4f0a6bc289fdcf4..6ad7e28371f3d73dfba4d67ff5a61f5dd1d98164 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -149,7 +149,8 @@ type identified_extended = {
 
 and identified_axiomatic = {
   iax_name : string;
-  iax_props : identified_property list
+  iax_props : identified_property list;
+  iax_attrs : attributes;
 }
 
 and identified_lemma = {