diff --git a/Makefile b/Makefile
index 49b29bb737853c53dbacb402a7853791203c3a1a..7bd0b4b674794a0b4f736712e03390161ec0fe25 100644
--- a/Makefile
+++ b/Makefile
@@ -526,8 +526,8 @@ KERNEL_CMO=\
 	src/kernel_services/ast_printing/cil_descriptive_printer.cmo    \
 	src/kernel_services/parsetree/cabs.cmo                               \
 	src/kernel_services/parsetree/cabshelper.cmo                         \
-	src/kernel_services/ast_printing/logic_print.cmo                \
 	src/kernel_services/ast_queries/logic_utils.cmo              \
+	src/kernel_services/ast_printing/logic_print.cmo                \
 	src/kernel_internals/parsing/logic_parser.cmo                  \
 	src/kernel_internals/parsing/logic_lexer.cmo                   \
 	src/kernel_services/ast_queries/logic_typing.cmo             \
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index fa18c2c8744144e0da2892d139faf1cda8e673e0..6f0ad747309650ac647c2d41ccb6c6a4f3eecbaa 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1699,15 +1699,15 @@ logic_def:
 | LEMMA poly_id COLON full_lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();
-      LDlemma (id, false, labels, tvars, toplevel_pred Assert $4) }
+      LDlemma (id, labels, tvars, toplevel_pred Assert $4) }
 | CHECK_LEMMA poly_id COLON full_lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();
-      LDlemma (id, false, labels, tvars, toplevel_pred Check $4) }
+      LDlemma (id, labels, tvars, toplevel_pred Check $4) }
 | ADMIT_LEMMA poly_id COLON full_lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();
-      LDlemma (id, false, labels, tvars, toplevel_pred Admit $4) }
+      LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
 | AXIOMATIC any_identifier LBRACE logic_decls RBRACE
     { LDaxiomatic($2,$4) }
 | TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
@@ -1780,7 +1780,7 @@ logic_decl:
 | AXIOM poly_id COLON full_lexpr SEMICOLON
     { let (id,labels,tvars) = $2 in
       exit_type_variables_scope ();
-      LDlemma (id, true, labels, tvars, toplevel_pred Assert $4) }
+      LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
 ;
 
 logic_decl_loc:
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 9f5080a17cfde646576a6b769ddd491a2792a84e..7fe064e19d786945e81b32f6ee274802dcadfd65 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -867,8 +867,8 @@ let rec global_annot_without_irrelevant_attributes ga =
   | Daxiomatic(n,l,attr,loc) ->
     Daxiomatic(n,List.map global_annot_without_irrelevant_attributes l,
                drop_attributes_for_merge attr,loc)
-  | Dlemma (id,ax,labs,typs,st,attr,loc) ->
-    Dlemma (id,ax,labs,typs,st,drop_attributes_for_merge attr,loc)
+  | Dlemma (id,labs,typs,st,attr,loc) ->
+    Dlemma (id,labs,typs,st,drop_attributes_for_merge attr,loc)
   | Dtype (lti,loc) ->
     Dtype (logic_type_info_without_irrelevant_attributes lti, loc)
   | Dextended (ext, attr, loc) ->
@@ -941,10 +941,10 @@ let rec global_annot_pass1 g = match g with
     ignore (PlainMerging.getNode ltEq ltSyn !currentFidx info.lt_name info
               (Some (l, !currentDeclIdx)))
 
-  | Dlemma (n,is_ax,labs,typs,st,attr,l) ->
+  | Dlemma (n,labs,typs,st,attr,l) ->
     CurrentLoc.set l;
     ignore (PlainMerging.getNode
-              llEq llSyn !currentFidx n (n,(is_ax,labs,typs,st,attr,l))
+              llEq llSyn !currentFidx n (n,(labs,typs,st,attr,l))
               (Some (l, !currentDeclIdx)))
   | Dextended(ext,_,l) ->
     CurrentLoc.set l;
@@ -1569,15 +1569,15 @@ let matchLogicLemma oldfidx (oldid, _ as oldnode) fidx (id, _ as node) =
   let oldlnode = PlainMerging.getNode llEq llSyn oldfidx oldid oldnode None in
   let lnode = PlainMerging.getNode llEq llSyn fidx id node None in
   if oldlnode != lnode then begin
-    let (oldid,(oldax,oldlabs,oldtyps,oldst,oldattr,oldloc)) = oldlnode.ndata in
+    let (oldid,(oldlabs,oldtyps,oldst,oldattr,oldloc)) = oldlnode.ndata in
     let oldfidx = oldlnode.nfidx in
-    let (id,(ax,labs,typs,st,attr,loc)) = lnode.ndata in
+    let (id,(labs,typs,st,attr,loc)) = lnode.ndata in
     let fidx = lnode.nfidx in
     let oldattr = drop_attributes_for_merge oldattr in
     let attr = drop_attributes_for_merge attr in
     if Logic_utils.is_same_global_annotation
-        (Dlemma (oldid,oldax,oldlabs,oldtyps,oldst,oldattr,oldloc))
-        (Dlemma (id,ax,labs,typs,st,attr,loc))
+        (Dlemma (oldid,oldlabs,oldtyps,oldst,oldattr,oldloc))
+        (Dlemma (id,labs,typs,st,attr,loc))
     then begin
       if oldfidx < fidx then
         lnode.nrep <- oldlnode.nrep
@@ -2375,7 +2375,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
           mergePushGlobals g
       | Some _ -> ()
     end
-  | Dlemma (n,_,_,_,_,_,l) ->
+  | Dlemma (n,_,_,_,_,l) ->
     begin
       CurrentLoc.set l;
       match PlainMerging.findReplacement true llEq !currentFidx n with
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 3e7cf2768e11f22a3b0ef9b1a9ec1e7f0c5f551b..a4ee7f3882e02ae8cf6d4ea3038de785fcbf24eb 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1827,10 +1827,9 @@ and global_annotation =
   | Daxiomatic of string * global_annotation list * attributes * location
   | Dtype of logic_type_info * location (** declaration of a logic type. *)
   | Dlemma of
-      string * bool * logic_label list * string list *
+      string * logic_label list * string list *
       toplevel_predicate * attributes * location
-  (** definition of a lemma. The boolean flag is [true] if the property should
-      be taken as an axiom and [false] if it must be proved.  *)
+  (** definition of all kinds of lemmas (axioms are admit lemmas).  *)
   | Dinvariant of logic_info * location
   (** global invariant. The predicate does not have any argument. *)
   | Dtype_annot of logic_info * location
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index da98bb2f64bd464a2f14d636c787995e4f3f751f..0cb64d24a9898703c24e347a8161aec4a942904d 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -132,8 +132,6 @@ and identified_lemma = {
   il_loc : location
 }
 
-and identified_axiom = identified_lemma
-
 and identified_instance = {
   ii_kf : kernel_function;
   ii_stmt : stmt;
@@ -162,7 +160,6 @@ and identified_other = {
 and identified_property =
   | IPPredicate of identified_predicate
   | IPExtended of identified_extended
-  | IPAxiom of identified_axiom
   | IPAxiomatic of identified_axiomatic
   | IPLemma of identified_lemma
   | IPBehavior of identified_behavior
@@ -237,7 +234,6 @@ let get_kinstr = function
   | IPFrom {if_kinstr=ki}
   | IPReachable {ir_kinstr=ki}
   | IPDecrease {id_kinstr=ki} -> ki
-  | IPAxiom _
   | IPAxiomatic _
   | IPLemma _  -> Kglobal
   | IPOther {io_loc} -> ki_of_o_loc io_loc
@@ -265,7 +261,6 @@ let get_kf = function
   | IPFrom {if_kf=kf}
   | IPDecrease {id_kf=kf}
   | IPPropertyInstance {ii_kf=kf} -> Some kf
-  | IPAxiom _
   | IPAxiomatic _
   | IPLemma _ -> None
   | IPReachable {ir_kf} -> ir_kf
@@ -276,7 +271,6 @@ let get_kf = function
 let rec get_names = function
   | IPPredicate ip -> (Logic_const.pred_of_id_pred ip.ip_pred).pred_name
   | IPExtended { ie_ext = {ext_name = name} }
-  | IPAxiom { il_name = name }
   | IPAxiomatic { iax_name = name }
   | IPLemma { il_name = name }
   | IPBehavior { ib_bhv = {b_name = name} }
@@ -327,7 +321,6 @@ let rec location = function
      | _,(t :: _) -> t.it_content.term_loc)
   | IPFrom {if_from=(t, _)} -> t.it_content.term_loc
   | IPDecrease {id_variant=(t, _)} -> t.term_loc
-  | IPAxiom {il_loc} -> il_loc
   | IPAxiomatic {iax_props} ->
     (match iax_props with
      | [] -> Cil_datatype.Location.unknown
@@ -364,7 +357,6 @@ let get_behavior = function
   | IPAllocation {ial_bhv=Id_loop _}
   | IPAssigns {ias_bhv=Id_loop _}
   | IPFrom {if_bhv=Id_loop _}
-  | IPAxiom _
   | IPAxiomatic _
   | IPExtended _
   | IPLemma _
@@ -402,7 +394,7 @@ let rec has_status = function
   | IPCodeAnnot {ica_ca={annot_content}} -> has_status_ca annot_content
   | IPPropertyInstance {ii_ip} -> has_status ii_ip
   | IPOther _ | IPReachable _
-  | IPAxiom _ | IPAxiomatic _ | IPBehavior _
+  | IPAxiomatic _ | IPBehavior _
   | IPDisjoint _ | IPComplete _
   | IPAssigns _ | IPFrom _
   | IPAllocation _ | IPDecrease _ | IPLemma _
@@ -426,9 +418,10 @@ let rec pretty_ip fmt = function
       pretty_predicate_kind ip_kind
       Cil_printer.pp_identified_predicate ip_pred
   | IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
-  | IPAxiom {il_name} -> Format.fprintf fmt "axiom@ %s" il_name
   | IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
-  | IPLemma {il_name} -> Format.fprintf fmt "lemma@ %s" il_name
+  | IPLemma {il_name; il_pred} ->
+    Format.fprintf fmt "%a@ %s"
+      Cil_printer.pp_lemma_kind il_pred.tp_kind il_name
   | IPTypeInvariant {iti_name; iti_type} ->
     Format.fprintf fmt "invariant@ %s for type %a" iti_name
       Cil_printer.pp_typ iti_type
@@ -490,7 +483,6 @@ let rec hash_ip =
   in
   function
   | IPPredicate {ip_pred=x} -> Hashtbl.hash (1, x.ip_id)
-  | IPAxiom {il_name=x} -> Hashtbl.hash (2, (x:string))
   | IPAxiomatic {iax_name=x} -> Hashtbl.hash (3, (x:string))
   | IPLemma {il_name=x} -> Hashtbl.hash (4, (x:string))
   | IPCodeAnnot {ica_ca=ca} -> Hashtbl.hash (5, ca.annot_id)
@@ -531,7 +523,7 @@ let rec hash_ip =
   | IPExtended {ie_ext={ext_id}} -> Hashtbl.hash (18, ext_id)
 
 let reprs = [
-  IPAxiom {
+  IPLemma {
     il_name="";il_labels=[];il_args=[];
     il_pred=Logic_const.(toplevel_predicate ptrue);
     il_attrs=[];
@@ -581,7 +573,6 @@ include Datatype.Make_with_collections
         | IPPredicate {ip_pred=s1}, IPPredicate {ip_pred=s2} -> s1.ip_id = s2.ip_id
         | IPExtended {ie_ext={ext_id=i1}}, IPExtended {ie_ext={ext_id=i2}} ->
           Datatype.Int.equal i1 i2
-        | IPAxiom {il_name=s1}, IPAxiom {il_name=s2}
         | IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
         | IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
         | IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
@@ -622,7 +613,7 @@ include Datatype.Make_with_collections
           IPPropertyInstance {ii_kf=kf2;ii_stmt=s2;ii_ip=ip2} ->
           Kernel_function.equal kf1 kf2 &&
           Stmt.equal s1 s2 && equal ip1 ip2
-        | (IPPredicate _ | IPAxiom _ | IPExtended _ | IPAxiomatic _ | IPLemma _
+        | (IPPredicate _ | IPExtended _ | IPAxiomatic _ | IPLemma _
           | IPCodeAnnot _ | IPComplete _ | IPDisjoint _ | IPAssigns _
           | IPFrom _ | IPDecrease _ | IPBehavior _ | IPReachable _
           | IPAllocation _ | IPOther _ | IPPropertyInstance _
@@ -681,7 +672,6 @@ include Datatype.Make_with_collections
             if n = 0 then Stdlib.compare ba1 ba2 else n
           else
             n
-        | IPAxiom {il_name=s1}, IPAxiom {il_name=s2}
         | IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
         | IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
         | IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
@@ -701,14 +691,13 @@ include Datatype.Make_with_collections
             if c <> 0 then c else compare ip1 ip2
         | (IPPredicate _ | IPExtended _ | IPCodeAnnot _ | IPBehavior _ | IPComplete _ |
            IPDisjoint _ | IPAssigns _ | IPFrom _ | IPDecrease _ |
-           IPReachable _ | IPAxiom _ | IPAxiomatic _ | IPLemma _ |
+           IPReachable _ | IPAxiomatic _ | IPLemma _ |
            IPOther _ | IPAllocation _ | IPPropertyInstance _ |
            IPTypeInvariant _ | IPGlobalInvariant _) as x, y ->
           let nb = function
             | IPPredicate _ -> 1
             | IPAssigns _ -> 2
             | IPDecrease _ -> 3
-            | IPAxiom _ -> 4
             | IPAxiomatic _ -> 5
             | IPLemma _ -> 6
             | IPCodeAnnot _ -> 7
@@ -741,7 +730,6 @@ module Ordered_by_function = Datatype.Make_with_collections(
     let cmp_kind p1 p2 =
       let nb = function
         | IPAxiomatic _ -> 1
-        | IPAxiom _ -> 2
         | IPLemma _ -> 3
         | IPTypeInvariant _ -> 4
         | IPGlobalInvariant _ -> 5
@@ -772,8 +760,7 @@ module Ordered_by_function = Datatype.Make_with_collections(
     let rec cmp_same_kind p1 p2 =
       match (p1,p2) with
       | IPAxiomatic { iax_name = n1 }, IPAxiomatic { iax_name = n2 }
-      | IPAxiom { il_name = n1 }, IPAxiom { il_name = n2 }
-      | IPLemma { il_name = n1 }, IPAxiom { il_name = n2 }
+      | IPLemma { il_name = n1 }, IPLemma { il_name = n2 }
       | IPTypeInvariant { iti_name = n1 }, IPTypeInvariant { iti_name = n2 }
       | IPGlobalInvariant { igi_name = n1 },
         IPGlobalInvariant { igi_name = n2 }
@@ -859,7 +846,7 @@ let rec short_pretty fmt p = match p with
      | name :: _ -> Format.pp_print_string fmt name
      | [] -> pretty fmt p)
   | IPExtended {ie_ext={ext_name}} -> Format.pp_print_string fmt ext_name
-  | IPAxiom {il_name=n} | IPLemma {il_name=n}
+  | IPLemma {il_name=n}
   | IPTypeInvariant {iti_name=n} | IPGlobalInvariant {igi_name=n}
   | IPAxiomatic {iax_name=n} -> Format.pp_print_string fmt n
   | IPBehavior {ib_kf; ib_bhv={b_name}} ->
@@ -977,14 +964,6 @@ let rec pretty_debug fmt = function
       Cil_types_debug.pp_kinstr id_kinstr
       (Cil_types_debug.pp_option Cil_types_debug.pp_code_annotation) id_ca
       Cil_types_debug.pp_variant id_variant
-  | IPAxiom {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} ->
-    Format.fprintf fmt "IPAxiom(%a,%a,%a,%a,%a,%a)"
-      Cil_types_debug.pp_string il_name
-      (Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
-      (Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
-      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; iax_attrs} ->
     Format.fprintf fmt "IPAxiomatic(%a,%a,%a)"
       Cil_types_debug.pp_string iax_name
@@ -1154,11 +1133,10 @@ struct
       Format.asprintf  "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
     | IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
       let name = match ca.annot_content with
-        | AAssert (_, {tp_kind = Assert }) -> "assert"
-        | AAssert (_, {tp_kind = Check }) -> "check"
-        | AAssert (_, {tp_kind = Admit }) -> "admit"
-        | AInvariant (_,true,_) -> "loop_inv"
-        | AInvariant _ -> "inv"
+        | AAssert (_, {tp_kind}) -> Cil_printer.string_of_assert tp_kind
+        | AInvariant (_,loop,{tp_kind}) ->
+          let kw = if loop then "invariant" else "loop_invariant" in
+          Cil_printer.ident_of_predicate ~kw tp_kind
         | APragma _ -> "pragma"
         | AStmtSpec _ -> "contract"
         | AAssigns _ -> "assigns"
@@ -1178,11 +1156,11 @@ struct
       (kf_prefix kf) ^ "decr" ^ (variant_suffix variant)
     | IPDecrease {id_kf=kf; id_variant=variant} ->
       (kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
-    | IPAxiom {il_name=name; il_pred} ->
-      Format.asprintf "axiom_%s%a" name pp_names il_pred.tp_statement.pred_name
     | IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
     | IPLemma {il_name=name; il_pred} ->
-      Format.asprintf "lemma_%s%a" name pp_names il_pred.tp_statement.pred_name
+      Format.asprintf "%s_%s%a"
+        (Cil_printer.ident_of_lemma il_pred.tp_kind)
+        name pp_names il_pred.tp_statement.pred_name
     | IPTypeInvariant {iti_name; iti_pred} ->
       Format.asprintf "type_invariant_%s%a"
         iti_name pp_names iti_pred.pred_name
@@ -1190,10 +1168,10 @@ struct
       Format.asprintf "global_invariant_%s%a"
         igi_name pp_names igi_pred.pred_name
     | IPAllocation {ial_kf=kf; ial_kinstr=ki; ial_bhv=Id_contract (a,b)} ->
-      Format.asprintf "%s%s%a%salloc"
+      Format.asprintf "%s%s%a%sallocates"
         (kf_prefix kf) (ki_prefix ki) active_prefix a (behavior_prefix b)
     | IPAllocation {ial_kf=kf; ial_kinstr=Kstmt _; ial_bhv=Id_loop ca} ->
-      Format.asprintf "%sloop_alloc%a"
+      Format.asprintf "%sloop_allocates%a"
         (kf_prefix kf) pp_code_annot_names ca
     | IPAllocation _ -> assert false
     | IPAssigns {ias_kf=kf; ias_kinstr=ki; ias_bhv=Id_contract (a,b)} ->
@@ -1292,10 +1270,7 @@ struct
       add_part buffer p ; add_sep buffer ; add_parts buffer ps
 
   let prefix_with_kind tp name =
-    match tp.tp_kind with
-    | Assert -> name
-    | Check -> "check_" ^ name
-    | Admit -> "admit_" ^ name
+    Cil_printer.ident_of_predicate ~kw:name tp.tp_kind
 
   let rec parts_of_property ip : part list =
     match ip with
@@ -1355,11 +1330,7 @@ struct
                    ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
       [ K kf ; A ext_name ; S stmt ]
     | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_,p)}} ->
-      let a = match p.tp_kind with
-        | Assert -> "assert"
-        | Check -> "check"
-        | Admit -> "admit"
-      in
+      let a = Cil_printer.string_of_assert p.tp_kind in
       [K kf ; A a ; P p.tp_statement ]
     | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
       let a = prefix_with_kind p "loop_invariant" in
@@ -1391,10 +1362,9 @@ struct
     | IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt s; ir_program_point=After} ->
       [ K kf ; A "reachable_after" ; S s ]
 
-    | IPAxiomatic _
-    | IPAxiom _ -> []
+    | IPAxiomatic _ -> []
     | IPLemma {il_name=name; il_pred=p} ->
-      let a = prefix_with_kind p "lemma" in
+      let a = Cil_printer.ident_of_lemma p.tp_kind in
       [ A a ; A name ; P p.tp_statement ]
 
     | IPTypeInvariant {iti_name=name}
@@ -1476,7 +1446,7 @@ let ip_reachable_ppt p =
   let ir_kinstr = get_kinstr p in
   let ir_program_point = match p with
     | IPPredicate {ip_kind=(PKRequires _ | PKAssumes _ | PKTerminates)}
-    | IPAxiom _ | IPAxiomatic _ | IPLemma _ | IPComplete _
+    | IPAxiomatic _ | IPLemma _ | IPComplete _
     | IPDisjoint _ | IPCodeAnnot _ | IPAllocation _
     | IPDecrease _ | IPPropertyInstance _ | IPOther _
     | IPTypeInvariant _ | IPGlobalInvariant _
@@ -1630,7 +1600,6 @@ let ip_of_spec kf st ~active s =
   @ (Option.to_list (ip_terminates_of_spec kf st s))
   @ (Option.to_list (ip_decreases_of_spec kf st s))
 
-let ip_axiom s = IPAxiom s
 let ip_lemma s = IPLemma s
 let ip_type_invariant s = IPTypeInvariant s
 let ip_global_invariant s = IPGlobalInvariant s
@@ -1684,9 +1653,7 @@ let ip_of_global_annotation a =
     | Daxiomatic(iax_name, l, iax_attrs, _) ->
       let iax_props = List.fold_left aux [] l in
       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) ->
+    | Dlemma(il_name, il_labels, il_args, il_pred, il_attrs, il_loc) ->
       ip_lemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} :: acc
     | Dinvariant(l, igi_loc) ->
       let igi_pred = match l.l_body with
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index b712d764ed06d343bc450253476e571a8ce835f6..8c26d95abc56c6037c5797147a19a3c947abbb0e 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -162,8 +162,6 @@ and identified_lemma = {
   il_loc : location
 }
 
-and identified_axiom = identified_lemma
-
 (** Specialization of a property at a given point, identified by a statement
     and a function, along with the predicate transposed at this point (if it
     can be) and the original property. *)
@@ -195,7 +193,6 @@ and identified_other = {
 and identified_property = private
   | IPPredicate of identified_predicate
   | IPExtended of identified_extended
-  | IPAxiom of identified_axiom
   | IPAxiomatic of identified_axiomatic
   | IPLemma of identified_lemma
   | IPBehavior of identified_behavior
@@ -477,12 +474,6 @@ val ip_property_instance:
   kernel_function -> stmt -> Cil_types.identified_predicate option ->
   identified_property -> identified_property
 
-(** Builds an IPAxiom.
-    @since Carbon-20110201
-    @modify Oxygen-20120901 takes an identified_axiom instead of a string
-*)
-val ip_axiom: identified_axiom -> identified_property
-
 (** Build an IPLemma.
     @since Nitrogen-20111001
     @modify Oxygen-20120901 takes an identified_lemma instead of a string
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index a0719f99b8dbc95fcbcf0812861a3896a4e9109d..69eea3203070c39503ca52cb9bc79e10a9d2a722 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -353,7 +353,6 @@ let is_admitted_code_annot = function
   | _ -> false
 
 let rec is_admitted = function
-  | Property.IPAxiom _  -> true
   | Property.IPPredicate ip -> ip.ip_pred.ip_content.tp_kind = Admit
   | IPLemma lemma -> lemma.il_pred.tp_kind = Admit
   | IPCodeAnnot ca -> is_admitted_code_annot ca.ica_ca.annot_content
@@ -519,8 +518,9 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
   | Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
   | Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
   | Property.IPAllocation _ | Property.IPDecrease _ | Property.IPBehavior _
-  | Property.IPAxiom _ | Property.IPAxiomatic _ | Property.IPLemma _
-  | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ | Property.IPExtended _ ->
+  | Property.IPAxiomatic _ | Property.IPLemma _
+  | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _
+  | Property.IPExtended _ ->
     Kernel.fatal "unregistered property %a" Property.pretty ppt
 
 and logical_consequence e ppt hyps =
@@ -686,7 +686,7 @@ and get_status ?(must_register=true) ppt =
   | Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
   | Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
   | Property.IPDecrease _ | Property.IPAllocation _
-  | Property.IPAxiom _ | Property.IPAxiomatic _ | Property.IPLemma _
+  | Property.IPAxiomatic _ | Property.IPLemma _
   | Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ ->
     Kernel.fatal "trying to get status of unregistered property `%a'.\n\
                   That is forbidden (kernel invariant broken)."
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 48cf456eb780022c6d1146c3a2ef992050cdad90..951787b536a0f476d6946932eab7f175cad825d6 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -27,6 +27,53 @@ open Cil_datatype
 open Printer_api
 open Format
 
+let string_of_assert = function
+  | Assert -> "assert"
+  | Check -> "check"
+  | Admit -> "admit"
+
+let name_of_assert = function
+  | Assert -> "assertion"
+  | Check -> "check"
+  | Admit -> "admit"
+
+let string_of_lemma = function
+  | Assert -> "lemma"
+  | Check -> "check lemma"
+  | Admit -> "axiom"
+
+let ident_of_lemma = function
+  | Assert -> "lemma"
+  | Check -> "check_lemma"
+  | Admit -> "axiom"
+
+let string_of_predicate ~kw = function
+  | Assert -> kw
+  | Check -> "check " ^ kw
+  | Admit -> "admit " ^ kw
+
+let ident_of_predicate ~kw = function
+  | Assert -> kw
+  | Check -> "check_" ^ kw
+  | Admit -> "admit_" ^ kw
+
+let pp_assert_kind fmt kd = Format.pp_print_string fmt (string_of_assert kd)
+let pp_lemma_kind fmt kd = Format.pp_print_string fmt (string_of_lemma kd)
+let pp_predicate_kind ~kw fmt kd =
+  match kd with
+  | Assert -> Format.pp_print_string fmt kw
+  | Check ->
+    begin
+      Format.pp_print_string fmt "check " ;
+      Format.pp_print_string fmt kw ;
+    end
+  | Admit ->
+    begin
+      Format.pp_print_string fmt "admit " ;
+      Format.pp_print_string fmt kw ;
+    end
+
+
 module Extensions = struct
   let initialized = ref false
   let ref_print = ref (fun _ _ _ _ -> assert false)
@@ -2847,11 +2894,20 @@ class cil_printer () = object (self)
   method decreases fmt v = self#decrement "decreases" fmt v
   method variant fmt v = self#decrement "loop variant" fmt v
 
-  method private pp_predicate_kind fmt p =
-    match p.tp_kind with
+  method private pp_predicate_kind fmt = function
     | Assert -> ()
-    | Check -> fprintf fmt "%a " self#pp_acsl_keyword "check"
-    | Admit -> fprintf fmt "%a " self#pp_acsl_keyword "admit"
+    | Check -> self#pp_acsl_keyword fmt "check" ; pp_print_char fmt ' '
+    | Admit -> self#pp_acsl_keyword fmt "admit" ; pp_print_char fmt ' '
+
+  method private pp_lemma_kind fmt = function
+    | Assert -> self#pp_acsl_keyword fmt "lemma"
+    | Admit -> self#pp_acsl_keyword fmt "axiom"
+    | Check ->
+      begin
+        self#pp_acsl_keyword fmt "check" ;
+        pp_print_char fmt ' ' ;
+        self#pp_acsl_keyword fmt "lemma" ;
+      end
 
   method assumes fmt p =
     fprintf fmt "@[<hov 2>%a@ %a;@]"
@@ -2860,7 +2916,7 @@ class cil_printer () = object (self)
 
   method requires fmt p =
     fprintf fmt "@[<hov 2>%a%a@ %a;@]"
-      self#pp_predicate_kind p.ip_content
+      self#pp_predicate_kind p.ip_content.tp_kind
       self#pp_acsl_keyword "requires"
       self#identified_predicate p
 
@@ -2873,7 +2929,7 @@ class cil_printer () = object (self)
   method post_cond fmt (k,p) =
     let kw = get_termination_kind_name k in
     fprintf fmt "@[<hov 2>%a%a@ %a;@]"
-      self#pp_predicate_kind p.ip_content
+      self#pp_predicate_kind p.ip_content.tp_kind
       self#pp_acsl_keyword kw
       self#identified_predicate p
 
@@ -3086,14 +3142,9 @@ class cil_printer () = object (self)
     in
     match ca.annot_content with
     | AAssert (behav,p) ->
-      let kw = match p.tp_kind with
-        | Assert -> "assert"
-        | Check ->  "check"
-        | Admit ->  "admit"
-      in
       fprintf fmt "@[%a%a@ %a;@]"
         pp_for_behavs behav
-        self#pp_acsl_keyword kw
+        self#pp_acsl_keyword (string_of_assert p.tp_kind)
         self#predicate p.tp_statement
     | APragma (Slice_pragma sp) ->
       fprintf fmt "@[%a@ %a;@]"
@@ -3122,13 +3173,13 @@ class cil_printer () = object (self)
     | AInvariant(behav,true, i) ->
       fprintf fmt "@[<2>%a%a%a@ %a;@]"
         pp_for_behavs behav
-        self#pp_predicate_kind i
+        self#pp_predicate_kind i.tp_kind
         self#pp_acsl_keyword "loop invariant"
         self#predicate i.tp_statement
     | AInvariant(behav,false,i) ->
       fprintf fmt "@[<2>%a%a%a@ %a;@]"
         pp_for_behavs behav
-        self#pp_predicate_kind i
+        self#pp_predicate_kind i.tp_kind
         self#pp_acsl_keyword "invariant"
         self#predicate i.tp_statement
     | AVariant v ->
@@ -3217,12 +3268,11 @@ class cil_printer () = object (self)
         self#logic_var pred.l_var_info
         self#predicate (pred_body pred.l_body);
       current_label <- old_label
-    | Dlemma(name, is_axiom, labels, tvars, pred, _attr, _) ->
+    | Dlemma(name, labels, tvars, pred, _attr, _) ->
       (* attributes are meant to be purely internal for now. *)
       let old_lab = current_label in
-      fprintf fmt "@[<hv 2>@[<hov 1>%a%a %a%a%a:@]@ %t%a;@]@\n"
-        self#pp_predicate_kind pred
-        self#pp_acsl_keyword (if is_axiom then "axiom" else "lemma")
+      fprintf fmt "@[<hv 2>@[<hov 1>%a %a%a%a:@]@ %t%a;@]@\n"
+        self#pp_lemma_kind pred.tp_kind
         self#varname name
         self#labels labels
         self#polyTypePrms tvars
diff --git a/src/kernel_services/ast_printing/cil_printer.mli b/src/kernel_services/ast_printing/cil_printer.mli
index c6295e24517a60a0f85e65fc715cda531cdbfa1a..7e0b5fd02905c3441575f96375a3d1be1574db85 100644
--- a/src/kernel_services/ast_printing/cil_printer.mli
+++ b/src/kernel_services/ast_printing/cil_printer.mli
@@ -30,6 +30,34 @@
 
 include Printer_api.S
 
+(** ["assert"], ["check"] or ["admit"]. *)
+val string_of_assert : Cil_types.predicate_kind -> string
+
+(** ["assertion"], ["check"] or ["admit"]. *)
+val name_of_assert : Cil_types.predicate_kind -> string
+
+(** ["lemma"], ["check lemma"] or ["axiom"]. *)
+val string_of_lemma : Cil_types.predicate_kind -> string
+
+(** clause, prefixed by ["check"] or ["admit"]. *)
+val string_of_predicate : kw:string -> Cil_types.predicate_kind -> string
+
+(** same as [string_of_lemma] with ["_"] for separator. *)
+val ident_of_lemma : Cil_types.predicate_kind -> string
+
+(** same as [string_of_predicate] with ["_"] for separator. *)
+val ident_of_predicate : kw:string -> Cil_types.predicate_kind -> string
+
+(** pretty prints [string_of_assert]. *)
+val pp_assert_kind : Format.formatter -> Cil_types.predicate_kind -> unit
+
+(** pretty prints [string_of_lemma]. *)
+val pp_lemma_kind : Format.formatter -> Cil_types.predicate_kind -> unit
+
+(** pretty prints [string_of_predicate]. *)
+val pp_predicate_kind :
+  kw:string -> Format.formatter -> Cil_types.predicate_kind -> unit
+
 val get_termination_kind_name: Cil_types.termination_kind -> string
 
 val register_shallow_attribute: string -> unit
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 01097f0f0b676439aa128262b8fca99d2c224abe..e818857a279b7482830c58d6473fd2d73b6b910b 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1017,8 +1017,8 @@ and pp_global_annotation fmt = function
       pp_attributes attributes  pp_location location
   | Dtype(logic_type_info,location) ->
     Format.fprintf fmt "Dtype(%a,%a)"  pp_logic_type_info logic_type_info  pp_location location
-  | Dlemma(string,bool,logic_label_list,string_list,predicate,attributes,location) ->
-    Format.fprintf fmt "Dlemma(%a,%a,%a,%a,%a,%a,%a)"  pp_string string  pp_bool bool
+  | Dlemma(string,logic_label_list,string_list,predicate,attributes,location) ->
+    Format.fprintf fmt "Dlemma(%a,%a,%a,%a,%a,%a)"  pp_string string
       (pp_list pp_logic_label) logic_label_list (pp_list pp_string) string_list
       pp_toplevel_predicate predicate
       pp_attributes attributes  pp_location location
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index c9218dc6cff6925d90556f0e22c59e7dc42202a8..63119aba59ed84b535b975d90fd31a7d738ae5b7 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -120,13 +120,8 @@ let pp_top fmt tp = pp_named fmt tp.tp_statement
 let pp_code_annot fmt ca =
   match ca.annot_content with
   | AAssert(bs,tp) ->
-    let kind =
-      match tp.tp_kind with
-      | Assert -> "assertion"
-      | Check -> "check"
-      | Admit -> "admit"
-    in
-    Format.fprintf fmt "%s%a%a" kind pp_for bs pp_top tp
+    Format.fprintf fmt "%a%a%a"
+      Cil_printer.pp_assert_kind tp.tp_kind pp_for bs pp_top tp
   | AInvariant(bs,_,tp) ->
     Format.fprintf fmt "invariant%a%a" pp_for bs pp_top tp
   | AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
@@ -226,8 +221,11 @@ let pp_capitalize fmt s =
 let pp_acsl_extension fmt {ext_name} = pp_capitalize fmt ext_name
 
 let rec pp_prop kfopt kiopt kloc fmt = function
-  | IPAxiom {il_name=s} -> Format.fprintf fmt "Axiom '%s'" s
-  | IPLemma {il_name=s} -> Format.fprintf fmt "Lemma '%s'" s
+  | IPLemma {il_name=s; il_pred=p} ->
+    (match p.tp_kind with
+     | Admit -> Format.fprintf fmt "Axiom '%s'" s
+     | Assert -> Format.fprintf fmt "Lemma '%s'" s
+     | Check ->  Format.fprintf fmt "Check Lemma '%s'" s)
   | IPTypeInvariant {iti_name=s} -> Format.fprintf fmt "Type invariant '%s'" s
   | IPGlobalInvariant {igi_name=s} -> Format.fprintf fmt "Global invariant '%s'" s
   | IPAxiomatic {iax_name=s} -> Format.fprintf fmt "Axiomatic '%s'" s
@@ -500,7 +498,7 @@ let loop_order = function
 
 let rec ip_order = function
   | IPAxiomatic {iax_name=a} -> [I 0;S a]
-  | IPAxiom {il_name=a} | IPLemma {il_name=a} -> [I 1;S a]
+  | IPLemma {il_name=a} -> [I 1;S a]
   | IPOther {io_name=s;io_loc=OLContract kf} -> [I 3;F kf;S s]
   | IPOther {io_name=s;io_loc=OLStmt (kf, stmt)} -> [I 4;F kf;K (Kstmt stmt);S s]
   | IPOther {io_name=s;io_loc=OLGlob _} -> [I 5; S s]
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index d56af0ab52dbdbdbedfe0847f539ee4cfa7fb587..2c6c5a8ecee96fd92dcb751bc3e09e72f6182270 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -364,13 +364,9 @@ let rec print_decl fmt d =
       (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
       (pp_list ~sep:",@ " print_typed_ident) prms
       (pp_list ~sep:"@\n" print_case) cases
-  | LDlemma(name,is_axiom,labels,tvar,body) ->
-    fprintf fmt "@[<2>%s%a@ %s%a%a:@ %a;@]"
-      (match body.tp_kind with
-       | Assert -> ""
-       | Check ->  "check "
-       | Admit ->   "admit")
-      (pp_cond ~pr_false:"lemma" is_axiom) "axiom" name
+  | LDlemma(name,labels,tvar,body) ->
+    fprintf fmt "@[<2>%a@ %s%a%a:@ %a;@]"
+      Cil_printer.pp_lemma_kind body.tp_kind name
       (pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
       (pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
       print_lexpr body.tp_statement
@@ -422,12 +418,7 @@ let print_allocation ~isloop fmt fa =
 let print_clause name fmt e = fprintf fmt "@\n%s@ %a;" name print_lexpr e
 
 let print_tp_clause name fmt e =
-  let name =
-    match e.tp_kind with
-    | Assert -> name
-    | Check -> "check " ^ name
-    | Admit -> "admit " ^ name
-  in
+  let name = Cil_printer.string_of_predicate ~kw:name e.tp_kind in
   print_clause name fmt e.tp_statement
 
 let print_post fmt (k,e) =
@@ -493,23 +484,19 @@ let print_code_annot fmt ca =
   in
   match ca with
     AAssert(bhvs,e) ->
-    fprintf fmt "%a%s@ %a;"
+    fprintf fmt "%a%a@ %a;"
       print_behaviors bhvs
-      (match e.tp_kind with
-       | Assert -> ""
-       | Check ->  "check "
-       | Admit ->   "admit")
+      Cil_printer.pp_assert_kind e.tp_kind
       print_lexpr e.tp_statement
   | AStmtSpec (bhvs,s) ->
     fprintf fmt "%a%a"
       print_behaviors bhvs
       print_spec s
   | AInvariant (bhvs,loop,e) ->
-    fprintf fmt "%a%a%a%ainvariant@ %a;"
+    let kw = if loop then "loop invariant" else "invariant" in
+    fprintf fmt "%a%a@ %a;"
       print_behaviors bhvs
-      (pp_cond (e.tp_kind = Check)) "check @"
-      (pp_cond (e.tp_kind = Admit)) "admit @"
-      (pp_cond loop) "loop@ "
+      (Cil_printer.pp_predicate_kind ~kw) e.tp_kind
       print_lexpr e.tp_statement
   | AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
   | AAssigns (bhvs,a) ->
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index a23817a3be96cf8b08067ccda0783e2b22c8dc78..9989a671d839911fefad80bd78d5184f41161a6e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2113,11 +2113,11 @@ and childrenAnnotation vis a =
            Logic_env.add_logic_type ti'.lt_name ti')
         vis#get_filling_actions;
     if ti' != ti then Dtype (ti',loc) else a
-  | Dlemma(s,is_axiom,labels,tvars,p,attr,loc) ->
+  | Dlemma(s,labels,tvars,p,attr,loc) ->
     let p' = visitCilToplevel_predicate vis p in
     let attr' = visitCilAttributes vis attr in
     if p' != p || attr != attr' then
-      Dlemma(s,is_axiom,labels,tvars,p',attr',loc)
+      Dlemma(s,labels,tvars,p',attr',loc)
     else a
   | Dinvariant (p,loc) ->
     let p' = visitCilLogicInfo vis p in
@@ -5373,7 +5373,7 @@ let global_annotation_attributes = function
   | Dvolatile (_,_,_,attrs,_) -> attrs
   | Daxiomatic (_,_,attrs,_) -> attrs
   | Dtype ({ lt_attr }, _) -> lt_attr
-  | Dlemma (_,_,_,_,_,attrs,_) -> attrs
+  | Dlemma (_,_,_,_,attrs,_) -> attrs
   | Dinvariant ({l_var_info = { lv_attr }}, _) -> lv_attr
   | Dtype_annot ({l_var_info = { lv_attr }}, _) -> lv_attr
   | Dmodel_annot ({ mi_attr }, _) -> mi_attr
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index f76bde88d646113bb7715b96c2a40fd26cda4d6a..3a032c50e526be36d7334c04c83cc14eb547ad1a 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1987,7 +1987,7 @@ module Global_annotation = struct
           | Dtype(t1,_), Dtype(t2,_) -> Logic_type_info.compare t1 t2
           | Dtype _, _ -> -1
           | _, Dtype _ -> 1
-          | Dlemma (l1,_,_,_,_,attr1,_), Dlemma(l2,_,_,_,_,attr2,_) ->
+          | Dlemma (l1,_,_,_,attr1,_), Dlemma(l2,_,_,_,attr2,_) ->
             let res = Datatype.String.compare l1 l2 in
             if res = 0 then Attributes.compare attr1 attr2 else res
           | Dlemma _, _ -> -1
@@ -2022,7 +2022,7 @@ module Global_annotation = struct
           (* Empty axiomatic is weird but authorized. *)
           | Daxiomatic (_,g::_,_,_) -> 5 * hash g
           | Dtype (t,_) -> 7 * Logic_type_info.hash t
-          | Dlemma(n,_,_,_,_,_,_) -> 11 * Datatype.String.hash n
+          | Dlemma(n,_,_,_,_,_) -> 11 * Datatype.String.hash n
           | Dinvariant(l,_) -> 13 * Logic_info.hash l
           | Dtype_annot(l,_) -> 17 * Logic_info.hash l
           | Dmodel_annot(l,_) -> 19 * Model_info.hash l
@@ -2036,7 +2036,7 @@ module Global_annotation = struct
     | Dfun_or_pred(_, loc)
     | Daxiomatic(_, _, _, loc)
     | Dtype (_, loc)
-    | Dlemma(_, _, _, _, _, _, loc)
+    | Dlemma(_, _, _, _, _, loc)
     | Dinvariant(_, loc)
     | Dtype_annot(_, loc) -> loc
     | Dmodel_annot(_, loc) -> loc
@@ -2048,7 +2048,7 @@ module Global_annotation = struct
     | Dfun_or_pred({ l_var_info = { lv_attr }}, _) -> lv_attr
     | Daxiomatic(_, _, attr, _) -> attr
     | Dtype ({lt_attr}, _) -> lt_attr
-    | Dlemma(_, _, _, _, _, attr, _) -> attr
+    | Dlemma(_, _, _, _, attr, _) -> attr
     | Dinvariant({ l_var_info = { lv_attr }}, _) -> lv_attr
     | Dtype_annot({ l_var_info = { lv_attr}}, _) -> lv_attr
     | Dmodel_annot({ mi_attr }, _) -> mi_attr
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index f72ed2f586601fbe5d292d42c7a95db6474217ab..b8e8cae1f28b5a1714c302d37e24b493903d9d5e 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -1083,7 +1083,7 @@ module Base_checker = struct
                "field %s of type %a is not present in environment"
                mi.mi_name Printer.pp_typ mi.mi_base_type);
           Cil.DoChildren
-        | Dlemma(_,_,labels,_,_,_,_) ->
+        | Dlemma(_,labels,_,_,_,_) ->
           let old_labels = logic_labels in
           logic_labels <- labels @ logic_labels;
           Cil.DoChildrenPost (fun g -> logic_labels <- old_labels; g)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index a5167acba4e72fcbf795a23d8d97c4df4231aa9d..10e1c9714402301d3b9d452b19c3c6c9ab804a92 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4188,19 +4188,16 @@ struct
         C.error loc "Definition of %s is cyclic" s;
       my_info.lt_def <- tdef;
       Dtype (my_info,loc)
-    | LDlemma (x,is_axiom, labels, poly, {tp_kind = kind; tp_statement = e}) ->
+    | LDlemma (x,labels, poly, {tp_kind = kind; tp_statement = e}) ->
       if Logic_env.Lemmas.mem x then begin
         let old_def = Logic_env.Lemmas.find x in
+        let old_kind = match old_def with
+          | Dlemma(_,_,_,{tp_kind },_,_) -> tp_kind
+          | _ -> Assert in
         let old_loc = Cil_datatype.Global_annotation.loc old_def in
-        let is_axiom =
-          match old_def with
-          | Dlemma(_, is_axiom, _, _, _, _, _) -> is_axiom
-          | _ ->
-            Kernel.fatal ~current:true
-              "Logic_env.get_lemma must return Dlemma"
-        in
-        C.error loc "%s is already registered as %s (%a)"
-          x (if is_axiom then "axiom" else "lemma")
+        C.error loc "%a %s is already registered as %a (%a)"
+          Cil_printer.pp_lemma_kind kind x
+          Cil_printer.pp_lemma_kind old_kind
           Cil_datatype.Location.pretty old_loc
       end;
       let labels,env = annot_env loc labels poly in
@@ -4209,7 +4206,7 @@ struct
         | None -> labels
         | Some lab -> [lab]
       in
-      let def = Dlemma (x,is_axiom, labels, poly,  p, [], loc) in
+      let def = Dlemma (x,labels, poly,  p, [], loc) in
       Logic_env.Lemmas.add x def;
       def
     | LDinvariant (s, e) ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c62a3c86569cc1d00da7e311c46a70bb14487735..e568ddfc6aa1980f10b3d288ff3378fd865161f2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -723,8 +723,8 @@ let rec add_attribute_glob_annot a g =
     Daxiomatic(n,List.map (add_attribute_glob_annot a) l,
                Cil.addAttribute a al,loc)
   | Dtype(ti,_) -> ti.lt_attr <- Cil.addAttribute a ti.lt_attr; g
-  | Dlemma(n,ax,labs,t,p,al,l) ->
-    Dlemma(n,ax,labs,t,p,Cil.addAttribute a al,l)
+  | Dlemma(n,labs,t,p,al,l) ->
+    Dlemma(n,labs,t,p,Cil.addAttribute a al,l)
   | Dmodel_annot (mi,_) -> mi.mi_attr <- Cil.addAttribute a mi.mi_attr; g
   | Dcustom_annot(c,n,al,l) -> Dcustom_annot(c,n,Cil.addAttribute a al, l)
   | Dextended (e,al,l) -> Dextended(e,Cil.addAttribute a al,l)
@@ -1233,9 +1233,9 @@ let rec is_same_global_annotation ga1 ga2 =
     id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
     && is_same_attributes attr1 attr2
   | Dtype (t1,_), Dtype (t2,_) -> is_same_logic_type_info t1 t2
-  | Dlemma(n1,ax1,labs1,typs1,st1,attr1,_),
-    Dlemma(n2,ax2,labs2,typs2,st2,attr2,_) ->
-    is_same_string n1 n2 && ax1 = ax2 &&
+  | Dlemma(n1,labs1,typs1,st1,attr1,_),
+    Dlemma(n2,labs2,typs2,st2,attr2,_) ->
+    is_same_string n1 n2 &&
     is_same_list is_same_logic_label labs1 labs2 &&
     is_same_list (=) typs1 typs2 && is_same_toplevel_predicate st1 st2 &&
     is_same_attributes attr1 attr2
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 8b256a5861ac5a9a6f466fc2b88bd70a0dc5312c..e3c35f61facb2f144660b9b35cdf876f42cece9d 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -233,13 +233,12 @@ and decl_node =
         (** [LDinductive_def(name,labels,type_params, parameters, indcases)]
             represents an inductive definition of a new predicate.
          *)
-  | LDlemma of string * bool * string list * string list * toplevel_predicate
-      (** LDlemma(name,is_axiom,labels,type_params,property) represents
-          a lemma or an axiom [name].
-          [is_axiom] is true for an axiom and false for a lemma. [labels]
-          is the list of label arguments and
-          [type_params] the list of type parameters. Last, [property] is the
-          statement of the lemma.
+  | LDlemma of string * string list * string list * toplevel_predicate
+      (** LDlemma(name,labels,type_params,property) represents axioms and
+          lemmas. Axioms and admit lemmas are fusionned.
+          [labels] is the list of label arguments and
+          [type_params] the list of type parameters.
+          Last, [property] is the statement of the lemma.
        *)
   | LDaxiomatic of string * decl list
         (** [LDaxiomatic(id,decls)]
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index bc8cbae3b40e7dfaa4c8177cd43e4b89d81bf332..077cc38480e28e1258dddc52da8e8a90c8f34608 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1080,7 +1080,7 @@ let mk_deterministic_lemma () =
     let prop = Logic_const.toplevel_predicate ~kind:Check prop in
     let name = state.Promelaast.name ^ "_deterministic_trans" in
     let lemma =
-      Dlemma (name, false, [label],[],prop,[],Cil_datatype.Location.unknown)
+      Dlemma (name, [label],[],prop,[],Cil_datatype.Location.unknown)
     in
     Annotations.add_global Aorai_option.emitter lemma
   in
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 68ac1d09272ba705d7f0c0d23c19f2a5de4ce938..d29eb062dfc7511d8298b2371658f78012199247 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -499,14 +499,12 @@ let to_do_on_select
         "This is a complete behaviors clause.@.%a@."
         pretty_predicate_status ip;
       main_ui#view_original (location ip)
-    | PIP(IPAxiom _ as ip) ->
-      main_ui#pretty_information "This is an axiom.@.";
-      main_ui#view_original (location ip)
     | PIP(IPAxiomatic _ as ip) ->
       main_ui#pretty_information "This is an axiomatic.@.";
       main_ui#view_original (location ip)
-    | PIP(IPLemma _ as ip) ->
-      main_ui#pretty_information "This is a lemma.@.";
+    | PIP(IPLemma { il_pred } as ip) ->
+      main_ui#pretty_information "This is a %a.@."
+        Cil_printer.pp_lemma_kind il_pred.tp_kind;
       main_ui#view_original (location ip)
     | PIP(IPTypeInvariant _ as ip) ->
       main_ui#pretty_information "This is a type invariant.@.";
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index c48c7e78696386bba640e6c39d5f23af094fe45b..a0be9aeb2d40cc93e900292886fcb52c53dbce41 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -316,7 +316,7 @@ module MYTREE = struct
     | Dvolatile _ -> Some "volatile clause"
     | Daxiomatic (s, _, _,_) -> Some (global_name s)
     | Dtype (lti, _) -> Some (global_name lti.lt_name)
-    | Dlemma (s, _, _, _, _, _,_) -> Some (global_name s)
+    | Dlemma (s, _, _, _, _,_) -> Some (global_name s)
     | Dinvariant (li, _) -> Some (global_name li.l_var_info.lv_name)
     | Dtype_annot (li, _) -> Some (global_name li.l_var_info.lv_name)
     | Dmodel_annot (mf, _) -> Some (global_name mf.mi_name)
diff --git a/src/plugins/gui/history.ml b/src/plugins/gui/history.ml
index 612c17011c1d279d86068a499abbd467b85bfe7a..29faae0a64ef52297423ec4fb00ee6f53fb12f0b 100644
--- a/src/plugins/gui/history.ml
+++ b/src/plugins/gui/history.ml
@@ -224,8 +224,8 @@ let translate_history_elt old_helt =
          GAnnot(Dtype(               {lt_name = new_name},_)  ,        new_loc))
       | (GAnnot(Daxiomatic(          old_name,_,_,_),                  old_loc),
          GAnnot(Daxiomatic(          new_name,_,_,_),                  new_loc))
-      | (GAnnot(Dlemma(              old_name,_,_,_,_,_,_),            old_loc),
-         GAnnot(Dlemma(              new_name,_,_,_,_,_,_),            new_loc))
+      | (GAnnot(Dlemma(              old_name,_,_,_,_,_),              old_loc),
+         GAnnot(Dlemma(              new_name,_,_,_,_,_),              new_loc))
       | (GAnnot(Dfun_or_pred({l_var_info= {lv_name=old_name}},_),      old_loc),
          GAnnot(Dfun_or_pred({l_var_info= {lv_name=new_name}},_),      new_loc))
 
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 6d42ff1688cfc5c625b82b1da41e4eb3831f24de..167e9afbb7f1b8a4274a68ed40b26f67fb57a6bb 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -633,7 +633,6 @@ let make_panel (main_ui:main_window_extension_points) =
     | IPPredicate {ip_kind=PKEnsures _;ip_kinstr=Kstmt _} ->
       ensures.get() && stmtSpec.get()
     | IPPredicate {ip_kind = PKTerminates} -> terminates.get ()
-    | IPAxiom _ -> false
     | IPTypeInvariant _ -> typeInvariants.get()
     | IPGlobalInvariant _ -> globalInvariants.get()
     | IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index e78913fabfae93985a69fb84ff131f448f6124a5..e488ba9e61c68732db77ba52d3cc9621eba803db 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -79,9 +79,9 @@ let make_axiomatic_is_allocable loc () =
   let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
   let app = pnot (papp (is_allocable,[label],[t_i])) in
   let prop = pforall ([lv_i], pimplies (cond, app)) in
-  let prop = Logic_const.toplevel_predicate prop in
+  let prop = Logic_const.toplevel_predicate ~kind:Admit prop in
   let gfun = Dfun_or_pred(is_allocable, loc) in
-  let axiom = Dlemma("never_allocable", true, [label],[],prop,[], loc) in
+  let axiom = Dlemma("never_allocable", [label],[],prop,[], loc) in
   ("dynamic_allocation", [gfun ; axiom]), [is_allocable]
 
 let get_is_allocable loc =
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index eab39c256c876df25e86fffe38c0851db387c58c..12d64ad6e94bf30041c359bf8bb4d705e75a29f7 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -149,8 +149,7 @@ let ip_is_in_libc ip =
       match ip with
       | IPAxiomatic {iax_attrs=attrs}
       | IPLemma {il_attrs=attrs}
-      | IPAxiom {il_attrs=attrs} ->
-        Cil.is_in_libc attrs
+        -> Cil.is_in_libc attrs
       | _ ->
         false
     end
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 86a697b3b4ede3e7900c5efdfbb427c3ee678b50..962ed38461e91ff9f4f4e810d6cd14f4b026b7bb 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -322,7 +322,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
         | Dvolatile (_, _, _, _, _) -> " (Volatile) "
         | Daxiomatic (s, _, _, _) -> s
         | Dtype (lti, _) ->  lti.lt_name
-        | Dlemma (ln, _, _, _, _, _, _) ->  ln
+        | Dlemma (ln, _, _, _, _, _) ->  ln
         | Dinvariant (toto, _) -> toto.l_var_info.lv_name
         | Dtype_annot (ta, _) -> ta.l_var_info.lv_name
         | Dmodel_annot (mi, _) -> mi.mi_name
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 2179ef3b1aaad9aa77f53ece2bdcaa147c86986a..29ac575f1351bd484af3c203a4d113f82da83507 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -169,8 +169,8 @@ class visitor = object
     | Daxiomatic(str, _, _, _) ->
       warn "axiomatic" str;
       Cil.DoChildren
-    | Dlemma(str, axiom, _, _, _, _, _) ->
-      warn (if axiom then "axiom" else "lemma") str;
+    | Dlemma(str, _, _, { tp_kind }, _, _) ->
+      warn (Cil_printer.string_of_lemma tp_kind) str;
       Cil.DoChildren
     | _ ->
       Cil.DoChildren
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 4f005429106a4e0804a3137b4196bf34194a128e..1c6c22f3d644838f5ab6dbbe6e833784f446642e 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -432,7 +432,7 @@ let rec monitored_property ip =
   | IPDisjoint _ -> true
   | IPReachable {ir_kf=None} -> false
   | IPReachable {ir_kf=Some _} -> true
-  | IPAxiomatic _ | IPAxiom _ -> false
+  | IPAxiomatic _ -> false
   | IPLemma _ -> true
   | IPTypeInvariant _ | IPGlobalInvariant _ -> true
   | IPOther _ -> true
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 7139e9024396367c83c9dc4f27fbda745ecf4b6c..082623df4cebc301120cad492e68bd270ef5bb88 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -82,6 +82,7 @@ struct
   let t_axiomatic = t_kind "axiomatic" "Axiomatic definitions"
   let t_axiom = t_kind "axiom" "Logical axiom"
   let t_lemma = t_kind "lemma" "Logical lemma"
+  let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
 
   let p_ext = Enum.prefix kinds ~name:"ext" ~var:"<clause>"
       ~descr:(Md.plain "ACSL extension `<clause>`")
@@ -108,8 +109,9 @@ struct
       end
     | IPExtended { ie_ext={ ext_name } } -> Enum.instance p_ext ext_name
     | IPAxiomatic _ -> t_axiomatic
-    | IPAxiom _ -> t_axiom
-    | IPLemma _ -> t_lemma
+    | IPLemma { il_pred = { tp_kind = Admit } } -> t_axiom
+    | IPLemma { il_pred = { tp_kind = Assert } } -> t_lemma
+    | IPLemma { il_pred = { tp_kind = Check } } -> t_check_lemma
     | IPBehavior _ -> t_behavior
     | IPComplete _ -> t_complete
     | IPDisjoint _ -> t_disjoint
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index b179113b7056f653b3b7568e80f1c081248182f9..df303b0e2fc37676efd55611aa1699d2494b4365 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -588,9 +588,7 @@ module Make
 
   let code_annotation_text ca =
     match ca.annot_content with
-    | AAssert (_,{tp_kind = Assert}) ->  "assertion"
-    | AAssert (_,{tp_kind = Check}) -> "check"
-    | AAssert (_,{tp_kind = Admit}) -> "admit"
+    | AAssert (_,{tp_kind}) -> Cil_printer.name_of_assert tp_kind
     | AInvariant _ ->  "loop invariant"
     | APragma _  | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
     | AExtended _ ->
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 612bb0fc52699bd5af768f885e3fc93037c1dba5..5888b1bbe9b9c204ecae7582dd2e0eed4c86c9c6 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -41,7 +41,7 @@ let classify_pre_post kf ip =
   let open Property in
   match ip with
   | IPPredicate {ip_kind = PKEnsures (_, Normal)} -> Some (GL_Post kf)
-  | IPPredicate {ip_kind=PKEnsures _} | IPAxiom _ | IPAxiomatic _ | IPLemma _
+  | IPPredicate {ip_kind=PKEnsures _} | IPAxiomatic _ | IPLemma _
   | IPTypeInvariant _ | IPGlobalInvariant _
   | IPOther _ | IPCodeAnnot _ | IPAllocation _ | IPReachable _
   | IPExtended _
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index ce3237d2cf9b29f809e7987bdff589cec36a8b05..cb3647e4fde810b6212ce0a8e0351d24e2ee3a2f 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,9 +29,7 @@ let has_requires spec =
 
 let code_annotation_text ca =
   match ca.annot_content with
-  | AAssert (_, {tp_kind=Assert}) ->  "assertion"
-  | AAssert (_, {tp_kind=Check}) -> "check"
-  | AAssert (_, {tp_kind=Admit}) -> "admit"
+  | AAssert (_, {tp_kind}) -> Cil_printer.name_of_assert tp_kind
   | AInvariant _ ->  "loop invariant"
   | APragma _  | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
   | AExtended _  ->
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index d2fe872a4ec9de0e458db6c253c2f625f969a449..c61a714a1297b48227d80514487246a51f880d35 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -76,7 +76,7 @@ module LIT = WpContext.Generator(STR)
         define_lemma {
           l_name = prefix ^ "_literal" ;
           l_cluster = cluster () ;
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_types = 0 ;
           l_forall = [] ;
           l_triggers = [] ;
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 20c80248b99b5e3cbc82e60be032fd1e9705333c..5c8b21c9784d4b7ad35602673189459350cb5cae 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -157,7 +157,7 @@ module OPAQUE_COMP_BYTES_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
         } ;
         let min_size = if Cil.acceptEmptyCompinfo () then e_zero else e_one in
         Definitions.define_lemma {
-          l_kind = `Axiom ; l_name ;
+          l_kind = Admit ; l_name ;
           l_types = 0 ; l_triggers = [] ; l_forall = [] ;
           l_cluster = Definitions.compinfo c ;
           l_lemma = Lang.F.(p_leq min_size (e_fun size []))
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 31f11471323d8360196febc03c15cdc1fd2a35c3..57c44a2ff26ae2f58260256a85c5c249c0801f79 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -53,7 +53,7 @@ type cluster = {
 and dlemma = {
   l_name  : string ;
   l_cluster : cluster ;
-  l_kind : lkind ;
+  l_kind : predicate_kind ;
   l_types : int ;
   l_forall : var list ;
   l_triggers : trigger list list (* OR of AND triggers *) ;
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 36acb61bb5ab6a039286c27ffa957e95f59e3e7d..4bfe3071b85c5983d75af0e16cb4aa9835eadc73 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -48,7 +48,7 @@ type typedef = (tau,field,lfun) Qed.Engine.ftypedef
 type dlemma = {
   l_name  : string ;
   l_cluster : cluster ;
-  l_kind : lkind ;
+  l_kind : predicate_kind ;
   l_types : int ;
   l_forall : var list ;
   l_triggers : trigger list list ; (** OR of AND-triggers *)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 6273d95ac226bc6284e0ca10c5c837be3c02055f..31c18109ae01aec27ceb2ea4fc9c52291c090a14 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -71,7 +71,6 @@ let compute_ip cc ip =
       cc#compute
 
   | IPFrom _
-  | IPAxiom _
   | IPReachable _
   | IPPropertyInstance _
   | IPOther _
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 292f232b0d5250ddca68fb274db3fed800b03ec8..d2689aaefd605a6f52d8158f6d0807766fa581a4 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -543,7 +543,7 @@ struct
             let trigger = Trigger.of_term result in
             Definitions.define_lemma {
               l_name = name ;
-              l_kind = `Axiom ;
+              l_kind = Admit ;
               l_types = ldef.d_types ;
               l_forall = ldef.d_params ;
               l_triggers = [[trigger]] ;
@@ -725,7 +725,7 @@ struct
     (* Re-compile final cases *)
     let cases = List.map
         (fun (case,labels,types,lemma) ->
-           compile_lemma cluster ~kind:`Axiom case types labels lemma)
+           compile_lemma cluster ~kind:Admit case types labels lemma)
         cases in
     Definitions.update_symbol { ldef with d_definition = Inductive cases } ;
     type_for_signature l ldef sigp (* sufficient *) ; SIG sigm
@@ -774,7 +774,7 @@ struct
                     {
                       l_name ;
                       l_types = 0 ;
-                      l_kind = `Axiom ;
+                      l_kind = Admit ;
                       l_triggers = [frame.triggers] ;
                       l_forall = vs ;
                       l_cluster = cluster ;
@@ -805,9 +805,9 @@ struct
       Wp_parameters.warning ~source:l.lem_position
         "Lemma '%s' has labels, consider using global invariant instead."
         l.lem_name ;
+    let { tp_kind = kind ; tp_statement = p } = l.lem_predicate in
     Definitions.define_lemma
-      (compile_lemma c ~kind:l.lem_kind
-         l.lem_name l.lem_types l.lem_labels l.lem_property)
+      (compile_lemma c ~kind l.lem_name l.lem_types l.lem_labels p)
 
   let define_axiomatic cluster ax =
     begin
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 97e58671da3c495459958169aba187bda78e7b7e..c499f8273512dfd0d37bdadeb87968c4c66e8366 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -57,15 +57,12 @@ let trim name =
 (* --- Definition Blocks                                                  --- *)
 (* -------------------------------------------------------------------------- *)
 
-type lkind = [ `Axiom | `Check | `Lemma ]
-
 type logic_lemma = {
   lem_name : string ;
-  lem_kind : lkind ;
   lem_position : Filepath.position ;
   lem_types : string list ;
   lem_labels : logic_label list ;
-  lem_property : predicate ;
+  lem_predicate : toplevel_predicate ;
   lem_depends : logic_lemma list ;
   (* global lemmas declared before in AST order (in reverse order) *)
   lem_attrs : attributes ;
@@ -194,30 +191,21 @@ let pp_profile fmt l =
 (* -------------------------------------------------------------------------- *)
 
 let ip_lemma l =
-  let open Property in
-  let mk_prop, kind =
-    match l.lem_kind with
-    | `Axiom -> Property.ip_axiom, Admit
-    | `Lemma -> Property.ip_lemma, Assert
-    | `Check -> Property.ip_lemma, Check
-  in
-  mk_prop
-    {il_name = l.lem_name; il_labels = l.lem_labels;
-     il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
-     il_attrs = l.lem_attrs;
-     il_pred = Logic_const.toplevel_predicate ~kind l.lem_property}
+  Property.ip_lemma {
+    il_name = l.lem_name; il_labels = l.lem_labels;
+    il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
+    il_attrs = l.lem_attrs;
+    il_pred = l.lem_predicate;
+  }
 
 let lemma_of_global ~context = function
-  | Dlemma(name,axiom,labels,types,pred,attrs,loc) ->
-      let kind = if axiom then `Axiom else
-        if pred.tp_kind = Check then `Check else `Lemma in
+  | Dlemma(name,labels,types,pred,attrs,loc) ->
       {
         lem_name = name ;
         lem_position = fst loc ;
         lem_types = types ;
         lem_labels = labels ;
-        lem_kind = kind ;
-        lem_property = pred.tp_statement ;
+        lem_predicate = pred ;
         lem_depends = context ;
         lem_attrs = attrs ;
       }
@@ -418,7 +406,7 @@ class visitor =
       | Dlemma _ ->
           let lem = lemma_of_global database.proofcontext global in
           register_lemma database self#section lem ;
-          if lem.lem_kind <> `Check then
+          if Logic_utils.use_predicate lem.lem_predicate.tp_kind then
             database.proofcontext <- lem :: database.proofcontext ;
           SkipChildren
 
@@ -555,13 +543,9 @@ let pp_decl fmt d l =
       pp_sig fmt kind l ;
   end
 
-let pp_kind fmt = function
-  | `Axiom -> Format.pp_print_string fmt "axiom"
-  | `Lemma -> Format.pp_print_string fmt "lemma"
-  | `Check -> Format.pp_print_string fmt "check lemma"
-
 let pp_lemma fmt l =
-  Format.fprintf fmt " * %a '%s'@\n" pp_kind l.lem_kind l.lem_name
+  Format.fprintf fmt " * %a '%s'@\n"
+    Cil_printer.pp_lemma_kind l.lem_predicate.tp_kind l.lem_name
 
 let get_name l = compute () ; compute_logicname l
 
@@ -596,7 +580,7 @@ let dump () =
       SMap.iter
         (fun l (lem,s) ->
            Format.fprintf fmt " * %a '%s' in %a@\n"
-             pp_kind lem.lem_kind
+             Cil_printer.pp_lemma_kind lem.lem_predicate.tp_kind
              l pp_section s)
         d.lemmas ;
       Format.fprintf fmt "-------------------------------------------------@." ;
diff --git a/src/plugins/wp/LogicUsage.mli b/src/plugins/wp/LogicUsage.mli
index ba9f38841c3afaea8c32021e796887fe136a5d46..cc925fa2ff2bddb3b19ce76e79c014cca0839ebe 100644
--- a/src/plugins/wp/LogicUsage.mli
+++ b/src/plugins/wp/LogicUsage.mli
@@ -30,15 +30,12 @@ open Clabels
 
 val basename : varinfo -> string (** Trims the original name *)
 
-type lkind = [ `Axiom | `Check | `Lemma ]
-
 type logic_lemma = {
   lem_name : string ;
-  lem_kind : lkind ;
   lem_position : Filepath.position ;
   lem_types : string list ;
   lem_labels : logic_label list ;
-  lem_property : predicate ;
+  lem_predicate : toplevel_predicate ;
   lem_depends : logic_lemma list ; (** in reverse order *)
   lem_attrs : attributes ;
 }
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index d37bc22c74f5caaadac6a26564a483a9570b3d37..f3c129e00646eae99fa6f829d360c8066caeeb39 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -155,7 +155,7 @@ struct
                     prefix name Chunk.pretty chunk i in
                 let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
                 Definitions.define_lemma {
-                  l_kind = `Axiom ;
+                  l_kind = Admit ;
                   l_name ; l_types = 0 ;
                   l_triggers ;
                   l_forall = F.p_vars l_lemma ;
@@ -293,7 +293,7 @@ struct
             d_cluster = cluster ;
           } ;
           Definitions.define_lemma {
-            l_kind = `Axiom ;
+            l_kind = Admit ;
             l_name = name ; l_types = 0 ;
             l_forall = F.p_vars lemma ;
             l_triggers = [[Trigger.of_term va]] ;
@@ -390,7 +390,7 @@ struct
           let is_init_r = M.is_init_range sigma obj loc e_one in
           let lemma = p_equiv is_init_p is_init_r in
           Definitions.define_lemma {
-            l_kind = `Axiom ;
+            l_kind = Admit ;
             l_name = name ^ "_range" ; l_types = 0 ;
             l_forall = params ;
             l_triggers = [] ;
@@ -438,7 +438,7 @@ struct
             let is_init_r = M.is_init_range sigma obj loc len in
             let lemma = p_equiv is_init_p is_init_r in
             Definitions.define_lemma {
-              l_kind = `Axiom ;
+              l_kind = Admit ;
               l_name = name ^ "_range" ; l_types = 0 ;
               l_forall = params ;
               l_triggers = [] ;
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 2e654d549b7ae9c82df2e794848069a76030ead0..074692a5c4436985a790dd7d94dbcab7db1fc48d 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -193,14 +193,14 @@ let constructor ~basename ~params ~index ~addrof ~consistent =
       } ;
       Definitions.define_lemma {
         l_cluster = cluster ;
-        l_kind = `Axiom ;
+        l_kind = Admit ;
         l_name = Printf.sprintf "addrof_%s_%d" basename id ;
         l_forall = params ; l_types = 0 ; l_triggers = [] ;
         l_lemma = p_addrof ;
       } ;
       Definitions.define_lemma {
         l_cluster = cluster ;
-        l_kind = `Axiom ;
+        l_kind = Admit ;
         l_name = Printf.sprintf "consistent_%s_%d" basename id ;
         l_forall = params ; l_types = 0 ; l_triggers = [] ;
         l_lemma = p_consistent ;
@@ -208,7 +208,7 @@ let constructor ~basename ~params ~index ~addrof ~consistent =
       if p_index != F.p_true then
         Definitions.define_lemma {
           l_cluster = cluster ;
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = Printf.sprintf "index_%s_%d" basename id ;
           l_forall = params @ [k] ; l_types = 0 ; l_triggers = [] ;
           l_lemma = p_index ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index af0b4a9b0a5ec02d254f4c4fcee520a4bf1c9caa..6eb29aa7425b3634b0d6844c9d3c8d8747dfbedd 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -241,7 +241,7 @@ module OPAQUE_COMP_LENGTH = WpContext.Generator(Cil_datatype.Compinfo)
           d_definition = Logic result ;
         } ;
         Definitions.define_lemma {
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = "Positive_Length_of_" ^ Lang.comp_id c ;
           l_types = 0 ; l_triggers = [] ; l_forall = [] ;
           l_cluster = Definitions.compinfo c ;
@@ -460,7 +460,7 @@ module STRING = WpContext.Generator(LITERAL)
         let alloc = F.e_get m base in (* The size is alloc-1 *)
         let sized = Cstring.str_len cst (F.e_add alloc F.e_minus_one) in
         Definitions.define_lemma {
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = name ; l_types = 0 ;
           l_triggers = [] ; l_forall = [] ;
           l_lemma = p_forall [a] (p_imply m_linked sized) ;
@@ -471,7 +471,7 @@ module STRING = WpContext.Generator(LITERAL)
         let name = prefix ^ "_region" in
         let re = - Cstring.str_id cst in
         Definitions.define_lemma {
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = name ; l_types = 0 ; l_triggers = [] ; l_forall = [] ;
           l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
           l_cluster = Cstring.cluster () ;
@@ -488,7 +488,7 @@ module STRING = WpContext.Generator(LITERAL)
         let v = F.e_get (e_var m) addr in
         let read = F.p_equal c v in
         Definitions.define_lemma {
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = name ; l_types = 0 ; l_triggers = [] ;
           l_forall = [m;i] ;
           l_cluster = Cstring.cluster () ;
@@ -512,7 +512,7 @@ module STRING = WpContext.Generator(LITERAL)
         } ;
         Definitions.define_lemma {
           l_name = prefix ^ "_base" ;
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_types = 0 ; l_triggers = [] ; l_forall = [] ;
           l_lemma = F.p_lt base F.e_zero ;
           l_cluster = Cstring.cluster () ;
@@ -546,7 +546,7 @@ module BASE = WpContext.Generator(Varinfo)
         let name = prefix ^ "_region" in
         let re = if x.vglob then 0 else if x.vformal then 1 else 2 in
         Definitions.define_lemma {
-          l_kind = `Axiom ;
+          l_kind = Admit ;
           l_name = name ; l_types = 0 ; l_triggers = [] ; l_forall = [] ;
           l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
           l_cluster = cluster_globals () ;
@@ -570,7 +570,7 @@ module BASE = WpContext.Generator(Varinfo)
             let m_linked = p_call p_linked [m] in
             let base_size = p_equal (F.e_get m base) size in
             Definitions.define_lemma {
-              l_kind = `Axiom ;
+              l_kind = Admit ;
               l_name = name ; l_types = 0 ;
               l_triggers = [] ; l_forall = [] ;
               l_lemma = p_forall [a] (p_imply m_linked base_size) ;
@@ -591,7 +591,7 @@ module BASE = WpContext.Generator(Varinfo)
             let m_init = p_call p_cinits [m] in
             let init_prop = p_forall [a] (p_imply m_init init_access) in
             Definitions.define_lemma {
-              l_kind = `Axiom ;
+              l_kind = Admit ;
               l_name = prefix ^ "_init" ; l_types = 0 ;
               l_triggers = [] ; l_forall = [] ;
               l_lemma = init_prop ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 26880047e346ac54b76e279e368bbbddc34b1da0..803bf87115076503721d2446610b4cb13265dc57 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -945,11 +945,12 @@ class visitor (ctx:context) c =
       id, t
 
     method on_dlemma l =
-      let kind = Why3.Decl.(if l.l_kind = `Axiom then Paxiom else Plemma) in
-      let cnv = empty_cnv ctx in
-      let id, t = self#make_lemma cnv l in
-      let decl = Why3.Decl.create_prop_decl kind id t in
-      ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
+      if l.l_kind <> Check then
+        let kind = Why3.Decl.(if l.l_kind = Admit then Paxiom else Plemma) in
+        let cnv = empty_cnv ctx in
+        let id, t = self#make_lemma cnv l in
+        let decl = Why3.Decl.create_prop_decl kind id t in
+        ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
 
     method on_dfun d =
       Wp_parameters.debug ~dkey:dkey_api "Define %a@." Lang.Fun.pretty d.d_lfun ;
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index d3e123821a510982c7e0afedeae9249f0c246618..4413187be9efce693afa69a5795f59bdbcb68288 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -735,7 +735,7 @@ let compute_usage () =
   (* Usage in lemmas *)
   let u_lemmas =
     LogicUsage.fold_lemmas
-      (fun l -> E.cup (pred (mk_ctx()) l.lem_property)) E.bot
+      (fun l -> E.cup (pred (mk_ctx()) l.lem_predicate.tp_statement)) E.bot
   in
   (* initial state by kf *)
   let usage = Globals.Functions.fold (fun kf env ->
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index ec5e67757db8d4ed6381f4ce76c4088cc9d3856d..e8ed36e6a7e14b00cb30e55b2a6256150df7e35b 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1404,7 +1404,7 @@ struct
   let compile_lemma l = ignore (VCG.lemma l)
 
   let prove_lemma collection l =
-    if l.lem_kind <> `Axiom then
+    if Logic_utils.verify_predicate l.lem_predicate.tp_kind then
       begin
         let id = WpPropId.mk_lemma_id l in
         let def = VCG.lemma l in
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 95d36b8435031fd02c2478582dde0802257a47bf..3d520317fc0d9c15445a98c8712dc60e0a12eb07 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1145,7 +1145,7 @@ let add_global_annotations annots =
           "Global invariant not handled yet ('%s' ignored)"
           linfo.l_var_info.lv_name;
         ()
-    | Dlemma (name,_,_,_,p,_,_) ->
+    | Dlemma (name,_,_,p,_,_) ->
         if use_predicate p.tp_kind then
           WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
 
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e764ce6e12f13da36e8d0e34c1c172e9ea35fbf2..05ca307d17159ba9d542aeccebf2033da84ccdea 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -513,7 +513,6 @@ let user_prop_names p =
   | IPFrom _
   | IPAllocation _
   | IPAxiomatic _
-  | IPAxiom _
   | IPBehavior _
   | IPReachable _
   | IPPropertyInstance _
@@ -684,7 +683,6 @@ let annot_hints hs = function
 
 let property_hints hs =
   let open Property in function
-    | IPAxiom  {il_name; il_pred}
     | IPLemma  {il_name; il_pred} ->
         List.iter (add_required hs) (il_name::il_pred.tp_statement.pred_name)
     | IPBehavior _ -> ()
@@ -981,6 +979,10 @@ let merge_assign_info a1 a2 = match a1,a2 with
       Wp_parameters.fatal "Several assigns ?"
 
 
+(* -------------------------------------------------------------------------- *)
+(* --- Axioms                                                             --- *)
+(* -------------------------------------------------------------------------- *)
+
 type axiom_info = prop_id * LogicUsage.logic_lemma
 
 let mk_axiom_info lemma =
@@ -988,11 +990,7 @@ let mk_axiom_info lemma =
 
 let pp_axiom_info fmt (id,thm) =
   Format.fprintf fmt "(@[%a:@ %a@])" pp_propid id
-    Printer.pp_predicate thm.LogicUsage.lem_property
-
-(* -------------------------------------------------------------------------- *)
-(* --- Prop Splitter                                                      --- *)
-(* -------------------------------------------------------------------------- *)
+    Printer.pp_predicate thm.LogicUsage.lem_predicate.tp_statement
 
 (* -------------------------------------------------------------------------- *)
 (* --- Prop Splitter                                                      --- *)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index f4e12f47e74ad3a899d93b143b29c60ba6c85a63..a3e11ddd1d1e2f26fdc086dc4defd558932575a7 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -675,7 +675,7 @@ let add_all_axioms tbl =
   let rec do_g g =
     match g with
     | Daxiomatic (_ax_name, globs,_,_) -> do_globs globs
-    | Dlemma (name,_,_,_,_,_,_) ->
+    | Dlemma (name,_,_,_,_,_) ->
         let lem = LogicUsage.logic_lemma name in
         add_axiom tbl lem
     | _ -> ()
diff --git a/tests/builtins/oracle/memcpy.res.oracle b/tests/builtins/oracle/memcpy.res.oracle
index dd7e4c0161be1efb85073436c242f28b540cb3b0..2f999a73305848291580c8f7674418100e8ff5c0 100644
--- a/tests/builtins/oracle/memcpy.res.oracle
+++ b/tests/builtins/oracle/memcpy.res.oracle
@@ -996,6 +996,32 @@
 --- Global Properties
 --------------------------------------------------------------------------------
 
+[  Valid  ] Axiomatic 'MemChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemSet'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrLen'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrNCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsLen'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsNCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'dynamic_allocation'
+            by Frama-C kernel.
 [ Extern  ] Axiom 'memchr_def'
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'memcmp_strlen_left'
@@ -1066,32 +1092,6 @@
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'wmemchr_def'
             Unverifiable but considered Valid.
-[  Valid  ] Axiomatic 'MemChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemSet'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrLen'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrNCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WMemChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsLen'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsNCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'dynamic_allocation'
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'memcmp'
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 6be9aa2345755e88b527f989d55cdacf4734fe1a..02d4b53e0b88d1de3344dd38408a5e06a4b952bc 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -1124,6 +1124,51 @@
 --- Global Properties
 --------------------------------------------------------------------------------
 
+[  Valid  ] Axiomatic 'GetsLength'
+            axiomatic GetsLength
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemChr'
+            axiomatic MemChr
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemCmp'
+            axiomatic MemCmp
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemSet'
+            axiomatic MemSet
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrChr'
+            axiomatic StrChr
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrCmp'
+            axiomatic StrCmp
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrLen'
+            axiomatic StrLen
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrNCmp'
+            axiomatic StrNCmp
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            axiomatic WMemChr
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsChr'
+            axiomatic WcsChr
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsCmp'
+            axiomatic WcsCmp
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsLen'
+            axiomatic WcsLen
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsNCmp'
+            axiomatic WcsNCmp
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'format_length'
+            axiomatic format_length
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'pipe_streams'
+            axiomatic pipe_streams
+            by Frama-C kernel.
 [ Extern  ] Axiom 'memchr_def'
             axiom memchr_def
             Unverifiable but considered Valid.
@@ -1226,51 +1271,6 @@
 [ Extern  ] Axiom 'wmemchr_def'
             axiom wmemchr_def
             Unverifiable but considered Valid.
-[  Valid  ] Axiomatic 'GetsLength'
-            axiomatic GetsLength
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemChr'
-            axiomatic MemChr
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemCmp'
-            axiomatic MemCmp
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemSet'
-            axiomatic MemSet
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrChr'
-            axiomatic StrChr
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrCmp'
-            axiomatic StrCmp
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrLen'
-            axiomatic StrLen
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrNCmp'
-            axiomatic StrNCmp
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WMemChr'
-            axiomatic WMemChr
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsChr'
-            axiomatic WcsChr
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsCmp'
-            axiomatic WcsCmp
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsLen'
-            axiomatic WcsLen
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsNCmp'
-            axiomatic WcsNCmp
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'format_length'
-            axiomatic format_length
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'pipe_streams'
-            axiomatic pipe_streams
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'remove'
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index 42a86c5e8f0cac08a72672c4f4908283f3ef6737..70d52622e9915aa69db43a5d579cedd29410a89f 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -49,6 +49,36 @@
 --- Global Properties
 --------------------------------------------------------------------------------
 
+[  Valid  ] Axiomatic 'GetsLength'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'MemSet'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrLen'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'StrNCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WMemChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsChr'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsLen'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'WcsNCmp'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'format_length'
+            by Frama-C kernel.
+[  Valid  ] Axiomatic 'pipe_streams'
+            by Frama-C kernel.
 [ Extern  ] Axiom 'memchr_def'
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'memcmp_strlen_left'
@@ -117,36 +147,6 @@
             Unverifiable but considered Valid.
 [ Extern  ] Axiom 'wmemchr_def'
             Unverifiable but considered Valid.
-[  Valid  ] Axiomatic 'GetsLength'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'MemSet'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrLen'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'StrNCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WMemChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsChr'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsLen'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'WcsNCmp'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'format_length'
-            by Frama-C kernel.
-[  Valid  ] Axiomatic 'pipe_streams'
-            by Frama-C kernel.
 
 --------------------------------------------------------------------------------
 --- Properties of Function 'remove'
diff --git a/tests/spec/add_global.ml b/tests/spec/add_global.ml
index 0a8f954137c1f7f9ff583f8be0ef3e617fc3e0fc..ddb4d76221225860fa846fced0a6450a7d75f0e3 100644
--- a/tests/spec/add_global.ml
+++ b/tests/spec/add_global.ml
@@ -1,7 +1,7 @@
 open Cil_types
 
 let emitter =
-  Emitter.create "Fancy" [ Emitter.Global_annot ] ~correctness:[] ~tuning:[] 
+  Emitter.create "Fancy" [ Emitter.Global_annot ] ~correctness:[] ~tuning:[]
 
 class vis prj =
 object(self)
@@ -14,8 +14,8 @@ object(self)
         Daxiomatic
           ("MyAxiomatic",
            [ Dlemma(
-                 "myaxiom", true, [], [],
-                 Logic_const.(toplevel_predicate ptrue),
+                 "myaxiom", [], [],
+                 Logic_const.(toplevel_predicate ~kind:Admit ptrue),
                  [], Cil_datatype.Location.unknown)],
            [], Cil_datatype.Location.unknown)
       in
diff --git a/tests/spec/oracle/axiom_redef_bts1005.res.oracle b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
index dd1cd99891e96851a59e1b0c045639884d5b1623..01b443473c69f0239760d31fade993604a9b6f9b 100644
--- a/tests/spec/oracle/axiom_redef_bts1005.res.oracle
+++ b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/spec/axiom_redef_bts1005.i (no preprocessing)
 [kernel:annot-error] tests/spec/axiom_redef_bts1005.i:5: Warning: 
-  inj1 is already registered as axiom (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
+  axiom inj1 is already registered as axiom (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
 /* Generated by Frama-C */