diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 14bab523bb3df1f021425b97ceaeafbf8fb07137..7a15dce648818142cd98813462572deb20d9728f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2835,13 +2835,17 @@ 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_only_check fmt p =
+    if p.tp_only_check then fprintf fmt "%a " self#pp_acsl_keyword "check"
+
   method assumes fmt p =
     fprintf fmt "@[<hov 2>%a@ %a;@]"
       self#pp_acsl_keyword "assumes"
       self#identified_predicate p
 
   method requires fmt p =
-    fprintf fmt "@[<hov 2>%a@ %a;@]"
+    fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+      self#pp_only_check p.ip_content
       self#pp_acsl_keyword "requires"
       self#identified_predicate p
 
@@ -2853,7 +2857,8 @@ 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;@]"
+    fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+      self#pp_only_check p.ip_content
       self#pp_acsl_keyword kw
       self#identified_predicate p
 
@@ -3091,13 +3096,15 @@ class cil_printer () = object (self)
         pp_for_behavs behav
         (self#allocation ~isloop:true) af
     | AInvariant(behav,true, i) ->
-      fprintf fmt "@[<2>%a%a@ %a;@]"
+      fprintf fmt "@[<2>%a%a%a@ %a;@]"
         pp_for_behavs behav
+        self#pp_only_check i
         self#pp_acsl_keyword "loop invariant"
         self#predicate i.tp_statement
     | AInvariant(behav,false,i) ->
-      fprintf fmt "@[<2>%a%a@ %a;@]"
+      fprintf fmt "@[<2>%a%a%a@ %a;@]"
         pp_for_behavs behav
+        self#pp_only_check i
         self#pp_acsl_keyword "invariant"
         self#predicate i.tp_statement
     | AVariant v ->
@@ -3189,7 +3196,8 @@ class cil_printer () = object (self)
     | Dlemma(name, is_axiom, 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:@]@ %t%a;@]@\n"
+      fprintf fmt "@[<hv 2>@[<hov 1>%a%a %a%a%a:@]@ %t%a;@]@\n"
+        self#pp_only_check pred
         self#pp_acsl_keyword (if is_axiom then "axiom" else "lemma")
         self#varname name
         self#labels labels