diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index c02a126964259ed12cdceb977060569ca62eaed4..f06f0573b63623fbf2a2dae4f4e6b77ccbcc6170 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -94,6 +94,7 @@
         "breaks", BREAKS, false;
 	"case", CASE, true;
         "char", CHAR, true;
+        "check", CHECK, false;
         "complete", COMPLETE, false;
         "const", CONST, true;
         "continues", CONTINUES, false;
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 489cf83599cba3d1c347d9b5f45f835d5c7d29a2..4f81bcc7f2476868e7de78547d402440840a907e 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -247,7 +247,7 @@
 %token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
 %token ALLOCABLE FREEABLE FRESH
 %token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
-%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT SEMICOLON NULL EMPTY
+%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK SEMICOLON NULL EMPTY
 %token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
 %token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
 %token EXITS BREAKS CONTINUES RETURNS
@@ -1430,6 +1430,7 @@ beg_pragma_or_code_annotation:
 | SLICE {}
 | FOR {}
 | ASSERT {}
+| CHECK {}
 | INVARIANT {}
 | EXT_CODE_ANNOT {}
 ;
@@ -1442,7 +1443,9 @@ pragma_or_code_annotation:
 
 code_annotation:
 | ASSERT full_lexpr SEMICOLON
-      { fun bhvs -> AAssert (bhvs,$2) }
+      { fun bhvs -> AAssert (bhvs,Assert,$2) }
+| CHECK full_lexpr SEMICOLON
+      { fun bhvs -> AAssert (bhvs,Check,$2) }
 | INVARIANT full_lexpr SEMICOLON { fun bhvs -> AInvariant (bhvs,false,$2) }
 | EXT_CODE_ANNOT grammar_extension SEMICOLON
   { fun bhvs ->
@@ -1837,6 +1840,7 @@ is_acsl_decl_or_code_annot:
 | EXT_GLOBAL     { $1 }
 | ASSUMES   { "assumes" }
 | ASSERT    { "assert" }
+| CHECK     { "check" }
 | GLOBAL    { "global" }
 | IMPACT    { "impact" }
 | INDUCTIVE { "inductive" }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index eb3177307c5d71e8f9037b17f89cb6f1e121fded..320b570ab51b9afb1bfb86ab3e5f2376b03830db 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8605,7 +8605,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
               let alloca_bounds = Logic_const.pand ~loc:castloc (pos_size, max_size) in
               let alloca_bounds = { alloca_bounds with pred_name = ["alloca_bounds"] } in
               let annot =
-                Logic_const.new_code_annotation (AAssert ([], alloca_bounds))
+                Logic_const.new_code_annotation (AAssert ([], Assert, alloca_bounds))
               in
               (mkStmtOneInstr ~ghost ~valid_sid
                  (Code_annot (annot, castloc)),
@@ -9125,7 +9125,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
           let pfalse = { pfalse with pred_name = ["missing_return"] } in
           let assert_false () =
             let annot =
-              Logic_const.new_code_annotation (AAssert ([], pfalse))
+              Logic_const.new_code_annotation (AAssert ([], Assert, pfalse))
             in
             Cil.mkStmt ~ghost ~valid_sid (Instr(Code_annot(annot,loc)))
           in
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index f306e0798342e5a0978fa287bf881b43c9483dc7..2d52020ae408c3d0f22febebc4d5ce80263f006e 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -474,7 +474,9 @@ let xform_switch_block ?(keepSwitch=false) b =
                       xform_switch_stmt
                       rest break_dest cont_dest label_index 0
                 | p ->
-                  let a = Logic_const.new_code_annotation (AAssert ([],p)) in
+                  let a =
+                    Logic_const.new_code_annotation (AAssert ([], Assert, p))
+                  in
                   let assertion = mkStmt (Instr(Code_annot(a,l))) in
                   popn popstack;
                   assertion:: s ::
@@ -495,7 +497,9 @@ let xform_switch_block ?(keepSwitch=false) b =
                       xform_switch_stmt
                       rest break_dest cont_dest label_index 0
                 | p ->
-                  let a = Logic_const.new_code_annotation (AAssert([],p)) in
+                  let a =
+                    Logic_const.new_code_annotation (AAssert ([], Assert, p))
+                  in
                   let assertion = mkStmt (Instr(Code_annot(a,l))) in
                   popn popstack;
                   assertion :: s ::
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 7f2887414b80ed3d7d6138c0c35bf896499cfdfc..ec872584b89aa0763597f5401a811b42d81b92ef 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -315,7 +315,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
           match !returns_assert with
           | { pred_content = Ptrue } -> [s; sg]
           | p ->
-            let a = Logic_const.new_code_annotation (AAssert ([],p)) in
+            let a = Logic_const.new_code_annotation (AAssert ([],Assert,p)) in
             let sta = mkStmt (Instr (Code_annot (a,loc))) in
             if callback<>None then
               ( let gclause = sta , a in
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 7038bbce318da3fdf1a9a6541b73a257930490db..fd73d9c1eb22c83d8d33bb3711085d7f4f39b6c6 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -206,7 +206,7 @@ let variant_predicate stmt v =
   Logic_const.pand ~loc (pred1, pred2)
 
 let supported_annotation annot = match annot.annot_content with
-  | AAssert ([], _)
+  | AAssert ([], _, _)
   | AInvariant ([], _, _)
   | AVariant (_, None) -> true
   | _ -> false (* TODO *)
@@ -216,7 +216,8 @@ let code_annot = Annotations.code_annot ~filter:supported_annotation
 let make_annotation kf stmt annot labels =
   let kind, pred =
     match annot.annot_content with
-    | AAssert ([], pred) -> Assert, pred
+    | AAssert ([], Cil_types.Assert, pred) -> Assert, pred
+    | AAssert ([], Cil_types.Check, pred) -> Check, pred
     | AInvariant ([], _, pred) -> Invariant, pred
     | AVariant (v, None) -> Assert, variant_predicate stmt v
     | _ -> assert false
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index e8af8bc2a58e2fde1a50c2f14031a506b46a3388..0baf4c9f58fed39b8debfc5323de3da60e620159 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -947,7 +947,7 @@ to function contracts."
         (* to preserve the effect of the statement *)
         pragmas :=
           { !pragmas with stmt = Stmt.Set.add ki !pragmas.stmt}
-      | AAssert (_behav,pred) ->
+      | AAssert (_behav,_,pred) ->
         (* to preserve the interpretation of the assertion *)
         get_zone_from_pred ki pred;
       | AInvariant (_behav,true,pred) -> (* loop invariant *)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index a33a5047ef460dc233a85e1afa1a0b4ffc6131f5..248d57078c094a74bcb2b58d5e0e205361a7d307 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -669,7 +669,7 @@ let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
 (*  Kernel.debug "registering alarm %a" D.pretty alarm;*)
   let add alarm =
     let pred = create_predicate ~loc alarm in
-    Logic_const.new_code_annotation (AAssert([], pred))
+    Logic_const.new_code_annotation (AAssert([], Assert, pred))
   in
   try
     let by_emitter = State.find kinstr in
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 8051b863e0d6e10256fff2665917d6a25abaa14f..684fcea7ce24a3b1e2749e43036b2b917b6df2d7 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1072,8 +1072,8 @@ let add_code_annot emitter ?kf stmt ca =
   let kf = find_englobing_kf ?kf stmt in
   let convert a =
     match a.annot_content with
-    | AAssert(l, p) ->
-      let a = { a with annot_content=AAssert(l,extend_name emitter p) } in
+    | AAssert(l, kind, p) ->
+      let a = { a with annot_content=AAssert(l,kind,extend_name emitter p) } in
       a, Property.ip_of_code_annot kf stmt a
     | AInvariant(l, b, p) ->
       let a={a with annot_content=AInvariant(l,b,extend_name emitter p)} in
@@ -1270,7 +1270,11 @@ let add_code_annot emitter ?kf stmt ca =
     Code_annots.add stmt tbl
 
 let add_assert e ?kf stmt a =
-  let a = Logic_const.new_code_annotation (AAssert ([],a)) in
+  let a = Logic_const.new_code_annotation (AAssert ([],Assert,a)) in
+  add_code_annot e ?kf stmt a
+
+let add_check e ?kf stmt a =
+  let a = Logic_const.new_code_annotation (AAssert ([],Check,a)) in
   add_code_annot e ?kf stmt a
 
 (** {3 Adding globals} *)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 3252d40e661210bc7754c71483567110d4a31abc..8e23a13514b40c60071a2b361d6628b460a3f7dc 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -281,6 +281,12 @@ val add_assert:
     provided, the function runs faster. 
     @plugin development guide *)
 
+val add_check:
+  Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
+(** Add a checking assertion attached to the given statement. If [kf] is
+    provided, the function runs faster.
+    @plugin development guide *)
+
 val add_global: Emitter.t -> global_annotation -> unit
 (** Add a new global annotation into the program. *)
 
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index f0eb6d86d0a0ea8d55cd9ac567a80295ffca5f28..9ca6bee84604575fe2f429beada46f30681d215f 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1739,11 +1739,17 @@ and pragma =
   | Slice_pragma of slice_pragma
   | Impact_pragma of impact_pragma
 
+(** Kind of an assertion:
+    - an assert is both evaluated and used as hypothesis afterwards;
+    - a check is only evaluated, but is not used as an hypothesis: it does not
+      affect the analyses. *)
+and assertion_kind = Assert | Check
+
 (** all annotations that can be found in the code.
     This type shares the name of its constructors with
     {!Logic_ptree.code_annot}. *)
 and code_annotation_node =
-  | AAssert of string list * predicate
+  | AAssert of string list * assertion_kind * predicate
   (** assertion to be checked. The list of strings is the list of
       behaviors to which this assertion applies. *)
 
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index ccba7c4f34b98bd4947c104ab47e58a8c5c390d9..2b35d02c825e07820bec0be9d2192080fe912288 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -628,7 +628,7 @@ let rec short_pretty fmt p = match p with
   | IPDisjoint (kf,_,_,_) ->
     Format.fprintf fmt "disjoint clause in function %a"
       Kernel_function.pretty kf
-  | IPCodeAnnot (_,_,{ annot_content = AAssert (_, { pred_name = name :: _ })}) ->
+  | IPCodeAnnot (_,_,{ annot_content = AAssert (_, _, { pred_name = name :: _ })}) ->
     Format.pp_print_string fmt name
   | IPCodeAnnot(_,_,{annot_content =
                        AInvariant (_,_, { pred_name = name :: _ })})->
@@ -845,7 +845,7 @@ struct
 
   let pp_code_annot_names fmt ca =
     match ca.annot_content with
-      | AAssert(for_bhv,named_pred) | AInvariant(for_bhv,_,named_pred) ->
+      | AAssert(for_bhv,_,named_pred) | AInvariant(for_bhv,_,named_pred) ->
         let pp_for_bhv fmt l =
           match l with
           | [] -> ()
@@ -907,7 +907,8 @@ struct
       Format.asprintf  "%sextended%a" (extended_loc_prefix le) pp_names [name]
     | IPCodeAnnot (kf,_, ca) ->
         let name = match ca.annot_content with
-          | AAssert _ -> "assert"
+          | AAssert (_, Assert, _) -> "assert"
+          | AAssert (_, Check, _) -> "check"
           | AInvariant (_,true,_) -> "loop_inv"
           | AInvariant _ -> "inv"
           | APragma _ -> "pragma"
@@ -1094,8 +1095,10 @@ struct
     | IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_,_)) } )
       -> [ K kf ; A clause ; S stmt ]
 
-    | IPCodeAnnot (kf,_, { annot_content = AAssert(_,p) } ) ->
+    | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Assert,p) } ) ->
       [K kf ; A "assert" ; P p ]
+    | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Check,p) } ) ->
+      [K kf ; A "check" ; P p ]
     | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,true,p) } ) ->
       [K kf ; A "loop_invariant" ; P p ]
     | IPCodeAnnot (kf,_, { annot_content = AInvariant(_,false,p) } ) ->
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 794e1cc8d4f85f7a6557b614e080cd2671c60663..99ae17d4e4a4c5e47a50e63c6953326711ed804e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2887,11 +2887,16 @@ class cil_printer () = object (self)
           (Pretty_utils.pp_list ~sep:",@ " pp_print_string) l
     in
     match ca.annot_content with
-    | AAssert (behav,p) ->
+    | AAssert (behav,Assert,p) ->
       fprintf fmt "@[%a%a@ %a;@]"
         pp_for_behavs behav
         self#pp_acsl_keyword "assert"
         self#predicate p
+    | AAssert (behav,Check,p) ->
+      fprintf fmt "@[%a%a@ %a;@]"
+        pp_for_behavs behav
+        self#pp_acsl_keyword "check"
+        self#predicate p
     | APragma (Slice_pragma sp) ->
       fprintf fmt "@[%a@ %a;@]"
         self#pp_acsl_keyword "slice pragma"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 029bb8bf79afab4827fed87758d55056bba87b69..c1c21886248bc6562a74e93dc5072bb4388b09a6 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -922,9 +922,13 @@ and pp_pragma pp_term fmt = function
   | Slice_pragma(term) -> Format.fprintf fmt "Slice_pragma(%a)" (pp_slice_pragma pp_term) term
   | Impact_pragma(term) -> Format.fprintf fmt "Impact_pragma(%a)" (pp_impact_pragma pp_term) term
 
+and pp_assertion_kind fmt = function
+  | Assert -> Format.pp_print_string fmt "Assert"
+  | Check -> Format.pp_print_string fmt "Check"
+
 and pp_code_annotation_node fmt = function
-  | AAssert(string_list,predicate) ->
-    Format.fprintf fmt "AAssert(%a,%a)"  (pp_list pp_string) string_list  pp_predicate predicate
+  | AAssert(string_list,kind,predicate) ->
+    Format.fprintf fmt "AAssert(%a,%a,%a)"  (pp_list pp_string) string_list pp_assertion_kind kind pp_predicate predicate
   | AStmtSpec(string_list,spec) ->
     Format.fprintf fmt "AStmtSpec(%a,%a)"  (pp_list pp_string) string_list  pp_spec spec
   | AInvariant(string_list,bool,predicate) ->
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index ade7c65cc86b8c94b7cacbb38c36a9cc19367c00..df0de122d9ac9582d9de2752500c68a022d37055 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -112,7 +112,10 @@ let pp_named fmt nx =
 
 let pp_code_annot fmt ca =
   match ca.annot_content with
-  | AAssert(bs,np) -> Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
+  | AAssert(bs,Assert,np) ->
+    Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
+  | AAssert(bs,Check,np) ->
+    Format.fprintf fmt "check%a%a" pp_for bs pp_named np
   | AInvariant(bs,_,np) ->
     Format.fprintf fmt "invariant%a%a" pp_for bs pp_named np
   | AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
@@ -250,11 +253,16 @@ let rec pp_prop kfopt kiopt kloc fmt = function
       pp_bhvs bs
       (pp_opt kiopt (pp_kinstr kloc)) ki
       (pp_opt kiopt pp_active) active
-  | IPCodeAnnot(_,_,{annot_content=AAssert(bs,np)}) ->
+  | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Assert,np)}) ->
     Format.fprintf fmt "Assertion%a%a%a"
       pp_for bs
       pp_named np
       (pp_kloc kloc) np.pred_loc
+  | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Check,np)}) ->
+    Format.fprintf fmt "Check%a%a%a"
+      pp_for bs
+      pp_named np
+      (pp_kloc kloc) np.pred_loc
   | IPCodeAnnot(_,_,{annot_content=AInvariant(bs,_,np)}) ->
     Format.fprintf fmt "Invariant%a%a%a"
       pp_for bs
@@ -348,13 +356,15 @@ let to_string pp elt =
   Buffer.contents b
 
 let code_annot_kind_and_node code_annot = match code_annot.annot_content with
-  | AAssert (_, {pred_content; pred_name}) ->
+  | AAssert (_, kind, {pred_content; pred_name}) ->
     let kind = match Alarms.find code_annot with
       | Some alarm -> Alarms.get_name alarm
       | None ->
         if List.exists ((=) "missing_return") pred_name
         then "missing_return"
-        else "user assertion"
+        else match kind with
+          | Assert -> "user assertion"
+          | Check -> "user check"
     in
     Some (kind, to_string Printer.pp_predicate_node pred_content)
   | AInvariant (_, _, {pred_content}) ->
@@ -456,7 +466,7 @@ let for_order k = function
   | [] -> [I k]
   | bs -> I (succ k) :: named_order bs
 let annot_order = function
-  | {annot_content=AAssert(bs,np)} ->
+  | {annot_content=AAssert(bs,_kind,np)} ->
     for_order 0 bs @ named_order np.pred_name
   | {annot_content=AInvariant(bs,_,np)} ->
     for_order 2 bs @ named_order np.pred_name
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 1de61b503727954aa7997505551792d4c91ea0c1..e74712d1ab373e5c949cd15d9063412fb58d239e 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -466,6 +466,10 @@ let print_pragma fmt p =
   | Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
   | Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
 
+let print_assertion_kind fmt = function
+  | Assert -> pp_print_string fmt "assert"
+  | Check -> pp_print_string fmt "check"
+
 let print_extension fmt (name, ext) =
   fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
 
@@ -474,8 +478,9 @@ let print_code_annot fmt ca =
     (pp_list ~pre:"for@ " ~sep:",@ " ~suf:":@ " pp_print_string) fmt bhvs
   in
   match ca with
-    AAssert(bhvs,e) ->
-    fprintf fmt "%aassert@ %a;" print_behaviors bhvs print_lexpr e
+    AAssert(bhvs,kind,e) ->
+    fprintf fmt "%a%a@ %a;"
+      print_behaviors bhvs print_assertion_kind kind print_lexpr e
   | AStmtSpec (bhvs,s) ->
     fprintf fmt "%a%a"
       print_behaviors bhvs
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 027a3758727e31a37b87840c49e4f65172cc7793..23e9a64223935754b638f38147a59a69cf90bf1c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3113,9 +3113,9 @@ and childrenSpec vis s =
    let vSpec s = visitCilFunspec vis s in
    let change_content annot = { ca with annot_content = annot } in
    match ca.annot_content with
-       AAssert (behav,p) ->
+       AAssert (behav,kind,p) ->
 	 let p' = vPred p in if p' != p then
-	   change_content (AAssert (behav,p'))
+	   change_content (AAssert (behav,kind,p'))
 	 else ca
      | APragma (Impact_pragma t) ->
 	 let t' = visitCilImpactPragma vis t in
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 17b141196aacedcb19746db9f02ac4d65c8a38aa..49792655353f2789c2cad7e88873e1f2ac7ea31c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2178,7 +2178,7 @@ module Code_annotation = struct
      end)
 
   let loc ca = match ca.annot_content with
-    | AAssert(_,{pred_loc=loc})
+    | AAssert(_,_,{pred_loc=loc})
     | AInvariant(_,_,{pred_loc=loc})
     | AVariant({term_loc=loc},_) -> Some loc
     | AAssigns _ | AAllocation _ | APragma _ | AExtended _
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 3b292cce6677521f1dceb355c4642eef80ab9781..af3f16c4a2766f9df561b3c5bf2ab20a4724e81a 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -648,7 +648,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
          names of statement contracts. *)
       if is_normalized then begin
         match ca.annot_content with
-        | AAssert(bhvs,_) | AStmtSpec(bhvs,_) | AInvariant (bhvs,_,_)
+        | AAssert(bhvs,_,_) | AStmtSpec(bhvs,_) | AInvariant (bhvs,_,_)
         | AAssigns(bhvs,_) | AAllocation(bhvs,_) | AExtended (bhvs,_,_) ->
           List.iter
             (fun b ->
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index a5a205947e2da1f126523a65eacaee1c753ddcef..e281a3b8920dd3e5aeb7273af369d2d90866d9e0 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3777,9 +3777,12 @@ struct
   let code_annot loc current_behaviors current_return_type ca =
     let source = fst loc in
     let annot = match ca with
-      | AAssert (behav,p) ->
+      | AAssert (behav,Assert,p) ->
         check_behavior_names loc current_behaviors behav;
-        Cil_types.AAssert (behav,predicate (code_annot_env()) p)
+        Cil_types.AAssert (behav, Cil_types.Assert, predicate (code_annot_env()) p)
+      | AAssert (behav,Check,p) ->
+        check_behavior_names loc current_behaviors behav;
+        Cil_types.AAssert (behav, Cil_types.Check, predicate (code_annot_env()) p)
       | APragma (Impact_pragma sp) ->
         Cil_types.APragma (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
       | APragma (Slice_pragma sp) ->
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 352824e171c1585f0746e879da519a37f82c871a..c99bcaee9a110f7dfb6d1c89390e686da30bebca 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1021,8 +1021,8 @@ let is_same_extension (_,e1,_,s1,c1) (_,e2,_,s2,c2) =
 
 let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
   match ca1.annot_content, ca2.annot_content with
-  | AAssert(l1,p1), AAssert(l2,p2) ->
-    is_same_list (=) l1 l2 && is_same_predicate p1 p2
+  | AAssert(l1,k1,p1), AAssert(l2,k2,p2) ->
+    is_same_list (=) l1 l2 && k1 = k2 && is_same_predicate p1 p2
   | AStmtSpec (l1,s1), AStmtSpec (l2,s2) ->
     is_same_list (=) l1 l2 && is_same_spec s1 s2
   | AInvariant(l1,b1,p1), AInvariant(l2,b2,p2) ->
@@ -2057,7 +2057,11 @@ let lhost_c_type thost =
      | _ -> assert false)
   | TResult ty -> ty
 
-let is_assert ca = match ca.annot_content with AAssert _ -> true | _ -> false
+let is_assert ca =
+  match ca.annot_content with AAssert (_, Assert, _) -> true | _ -> false
+
+let is_check ca =
+  match ca.annot_content with AAssert (_, Check, _) -> true | _ -> false
 
 let is_contract ca =
   match ca.annot_content with AStmtSpec _ -> true | _ -> false
@@ -2101,7 +2105,7 @@ let is_loop_annot s =
 
 let is_trivial_annotation a =
   match a.annot_content with
-  | AAssert (_,a) -> is_trivially_true a
+  | AAssert (_,_,a) -> is_trivially_true a
   | APragma _ | AStmtSpec _ | AInvariant _ | AVariant _
   | AAssigns _| AAllocation _ | AExtended _
     -> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index c5c7be4b017ea70d3b412c0fb03c8b6bea7939be..20f930b2b2f32927c1a016cafbea995c1e121da7 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -380,6 +380,7 @@ val clear_funspec: funspec -> unit
     a particular kind of annotations associated to a statement. *)
 
 val is_assert : code_annotation -> bool
+val is_check : code_annotation -> bool
 val is_contract : code_annotation -> bool
 val is_stmt_invariant : code_annotation -> bool
 val is_loop_invariant : code_annotation -> bool
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 50fcb567f702d5a7393eca2815b87e50bd6a5797..53907e6dc53d71f21bd0f3866f0a5e6b5a6f39b6 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -447,7 +447,7 @@ end = struct
           Printer.pp_code_annotation v;
         ChangeTo
           (Logic_const.new_code_annotation
-             (AAssert ([],
+             (AAssert ([], Assert,
                        { pred_name = []; pred_loc = Cil_datatype.Location.unknown;
                          pred_content = Ptrue})))
       end
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 3b97808c2aa5ec0230cd69ae7945420ea918677a..3461d6bd82a062519fb369c7f4e040b65a13ca7c 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -334,11 +334,13 @@ and pragma =
   | Slice_pragma of slice_pragma
   | Impact_pragma of impact_pragma
 
+and assertion_kind = Assert | Check
+
 
 (** all annotations that can be found in the code. This type shares the name of
     its constructors with {!Cil_types.code_annotation_node}. *)
 type code_annot =
-  | AAssert of string list * lexpr
+  | AAssert of string list * assertion_kind * lexpr
   (** assertion to be checked. The list of strings is the list of
       behaviors to which this assertion applies. *)
 
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index b64f3530965336676e0abe2f7855017ae6475bb3..007449cd839883d7bc0e23c04090445f2b2be633 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -488,7 +488,7 @@ let add_proven_annot (ca, stmt_ca) (ca_because, stmt_because) acc =
 let check_stmt_annots (ca, stmt_ca) stmt acc =
   let check _ annot acc =
     match ca.annot_content, annot.annot_content with
-    | AAssert (_, p'), AAssert (_, p) ->
+    | AAssert (_, Assert, p'), AAssert (_, _, p) ->
         if Logic_utils.is_same_predicate_node p.pred_content p'.pred_content then
           let acc, added = add_proven_annot (annot, stmt) (ca, stmt_ca) acc in
           if added then
@@ -574,7 +574,7 @@ class check_annot_visitor = object(self)
       Cil.get_original_stmt self#behavior (Extlib.the self#current_stmt)
     in
     begin match annot.annot_content with
-      | AAssert (_, _) ->
+      | AAssert _ ->
         R.debug ~level:2 "[check] annot %d at stmt %d in %a : %a@."
           annot.annot_id stmt.sid Kernel_function.pretty kf
           Printer.pp_code_annotation annot;
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 58e5b96280fd67851df297755143e0bfd2c0bd0e..0dc0cb5b874c64a708b1ed41c11ed7241fa7cd63 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -216,7 +216,7 @@ let local_printer: Printer.extensible_printer =
     method! code_annotation fmt ca =
       temporaries <- Cil_datatype.Varinfo.Set.empty;
       match ca.annot_content with
-      | AAssert(_, p) ->
+      | AAssert (_, _, p) ->
         (* ignore the ACSL name *)
         Format.fprintf fmt "@[<v>@[assert@ %a;@]" self#predicate_node p.pred_content;
         (* print temporary variables information *)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index c9e1050abf3cda4b83c8429a7bdcb8145d129bd5..304e26b6d01015d404145a18c98d2489f1e78edb 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -580,7 +580,8 @@ module Make
 
   let code_annotation_text ca =
     match ca.annot_content with
-    | AAssert _ ->  "assertion"
+    | AAssert (_, Assert, _) ->  "assertion"
+    | AAssert (_, Check, _) -> "check"
     | AInvariant _ ->  "loop invariant"
     | APragma _  | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
     | AExtended _ ->
@@ -599,7 +600,7 @@ module Make
   let interp_annot ~limit ~record kf ab stmt code_annot ~initial_state states =
     let ips = Property.ip_of_code_annot kf stmt code_annot in
     let source, _ = code_annotation_loc code_annot stmt in
-    let aux_interp code_annot behav p =
+    let aux_interp ~reduce code_annot behav p =
       let text = code_annotation_text code_annot in
       let in_behavior =
         match behav with
@@ -636,38 +637,41 @@ module Make
           msg_status status ~once:true ~source
             "%s%a got status %s." text Description.pp_named p message
         in
+        let reduce_state here res accstateset =
+          match res, in_behavior with
+          | _, `Unknown ->
+            (* Cannot conclude because behavior might be inactive *)
+            States.add here accstateset
+
+          | Alarmset.False, `True -> (* Dead/invalid branch *)
+            accstateset
+
+          | (Alarmset.Unknown | Alarmset.True), `True ->
+            let env = here_env ~pre:initial_state ~here in
+            (* Reduce by p if it is a disjunction, or if it did not
+               evaluate to True *)
+            let reduce = res = Alarmset.Unknown in
+            let reduced_states =
+              split_disjunction_and_reduce ~reduce ~limit env here p
+            in
+            fst (States.merge reduced_states ~into:accstateset)
+        in
         let reduced_states =
           States.fold
             (fun (here: Domain.t) accstateset ->
                let env = here_env ~pre:initial_state ~here in
                let res = Domain.evaluate_predicate env here p in
-               (* if record [holds], emit statuses in the Kernel,
-                  and print a message *)
+               (* if [record] holds, emit kernel status and print a message *)
                if record then emit res;
-               match res, in_behavior with
-               | _, `Unknown ->
-                 (* Cannot conclude because behavior might be inactive *)
-                 States.add here accstateset
-
-               | Alarmset.False, `True -> (* Dead/invalid branch *)
-                 accstateset
-
-               | (Alarmset.Unknown | Alarmset.True), `True ->
-                 let env = here_env ~pre:initial_state ~here in
-                 (* Reduce by p if it is a disjunction, or if it did not
-                    evaluate to True *)
-                 let reduce = res = Alarmset.Unknown in
-                 let reduced_states =
-                   split_disjunction_and_reduce ~reduce ~limit env here p
-                 in
-                 fst (States.merge reduced_states ~into:accstateset)
-            ) states States.empty
+               (* if [reduce] holds, reduce the state. *)
+               if reduce then reduce_state here res accstateset else accstateset)
+            states States.empty
         in
         (* States resulting from disjunctions are reversed compared to the
            'nice' ordering *)
-        States.reorder reduced_states
+        if reduce then States.reorder reduced_states else states
     in
-    let aux code_annot behav p =
+    let aux code_annot ~reduce behav p =
       if ignore_predicate p then
         states
       else if States.is_empty states then (
@@ -680,11 +684,12 @@ module Make
         end;
         states
       ) else
-        aux_interp code_annot behav p
+        aux_interp ~reduce code_annot behav p
     in
     match code_annot.annot_content with
-    | AAssert (behav,p)
-    | AInvariant (behav, true, p) -> aux code_annot behav p
+    | AAssert (behav, Check, p) -> aux ~reduce:false code_annot behav p
+    | AAssert (behav, Assert, p)
+    | AInvariant (behav, true, p) -> aux ~reduce:true code_annot behav p
     | APragma _
     | AInvariant (_, false, _)
     | AVariant _ | AAssigns _ | AAllocation _ | AExtended _
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index 4b807209ea73577e1a3e4bdd3e65cfab925630f6..a5d78c61b30a2e722f05c9d077547d68858f8b32 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -69,7 +69,7 @@ type red_alarm = {
 
 let get_predicate ca =
   match ca.annot_content with
-  | AAssert (_, p) -> { p with pred_name = [] }
+  | AAssert (_, _, p) -> { p with pred_name = [] }
   | _ -> assert false
 
 let make_red_alarm function_name ki alarm callstacks =
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 08eabb21cd9325eac38793407301dfa4287d6779..80d4d7ebce2766f4310fe98fcd23170f348f4543 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -454,7 +454,7 @@ module Select (Eval: Eval) = struct
         let lv = (Var vi, NoOffset) in
         select_lv main_ui (GL_Stmt (kf, stmt)) lv
       | PIP (IPCodeAnnot (kf, stmt,
-                          ({annot_content = AAssert (_, p) | AInvariant (_, true, p)} as ca)) as ip) ->
+                          ({annot_content = AAssert (_, _, p) | AInvariant (_, true, p)} as ca)) as ip) ->
         begin
           let loc = GL_Stmt (kf, stmt) in
           let alarm_or_property =
@@ -623,7 +623,7 @@ let add_keybord_shortcut_evaluate main_ui =
           select (find_loc kf fdec bl)
       end
     | PIP (Property.IPCodeAnnot (kf, stmt,
-                                 {annot_content = AAssert (_, _) | AInvariant (_, true, _)} )) ->
+                                 {annot_content = AAssert _ | AInvariant (_, true, _)} )) ->
       select (Some (GL_Stmt (kf, stmt)))
     | PIP (Property.IPPredicate (_, kf, Kglobal, _) as ip) ->
       select (Gui_eval.classify_pre_post kf ip)
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index e81cf164105c817b09af211696cd504a5c6ca7b7..6b2e67872412b52392079aef644e5f3242c5f8b9 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,7 +29,8 @@ let has_requires spec =
 
 let code_annotation_text ca =
   match ca.annot_content with
-  | AAssert _ ->  "assertion"
+  | AAssert (_, Assert, _) ->  "assertion"
+  | AAssert (_, Check, _) -> "check"
   | AInvariant _ ->  "loop invariant"
   | APragma _  | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
   | AExtended _  ->
@@ -202,7 +203,7 @@ let mark_green_and_red () =
        currently skipped during evaluation. *)
     if contains_c_at ca || (Alarms.find ca <> None) then
       match ca.annot_content with
-      | AAssert (_, p) | AInvariant (_, true, p) ->
+      | AAssert (_, _, p) | AInvariant (_, true, p) ->
         let loc = code_annotation_loc ca stmt in
         Cil.CurrentLoc.set loc;
         let kf = Kernel_function.find_englobing_kf stmt in
@@ -245,7 +246,7 @@ let mark_invalid_initializers () =
     | None -> ()
     | Some _ ->
       match ca.annot_content with
-      | AAssert (_, p) ->
+      | AAssert (_, _, p) ->
         let ip = Property.ip_of_code_annot_single kf first_stmt ca in
         (* Evaluate in a fully empty state. Only predicates that do not
            depend on the memory will result in 'False' *)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 81744b579a92317b77a4d957d7116ff5a5213165..3535467b5136d9c797a4b0236b18bd54bd202a00 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -902,7 +902,7 @@ let get_stmt_annots config v s =
               Printer.pp_code_annotation a;
             acc
           end
-    | AAssert (b_list,p) ->
+    | AAssert (b_list,_,p) ->
         let kf = config.kf in
         let acc = match is_annot_for_config config v s b_list with
           | TBRno -> acc
@@ -1385,7 +1385,7 @@ let get_id_prop_strategies ~model ?(assigns=WithAssigns) p =
   match p with
   | Property.IPCodeAnnot (kf,_,ca) ->
       let bhvs = match ca.annot_content with
-        | AAssert (l, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
+        | AAssert (l, _, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
         | _ -> []
       in get_strategies assigns kf model bhvs None (IdProp p)
   | Property.IPAssigns (kf, _, Property.Id_loop _, _)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7e3009c53bb7fe0117b0c4850da8094daff69536..da2f5d78db1ffb994455b28316fda97ad7debe28 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -420,7 +420,7 @@ let ident_names names =
                       | _ as n -> '\"' <> (String.get n 0) ) names
 
 let code_annot_names ca = match ca.annot_content with
-  | AAssert (_, named_pred)  -> "@assert"::(ident_names named_pred.pred_name)
+  | AAssert (_, _, named_pred)  -> "@assert"::(ident_names named_pred.pred_name)
   | AInvariant (_,_,named_pred) -> "@invariant"::(ident_names named_pred.pred_name)
   | AVariant (term, _) -> "@variant"::(ident_names term.term_name)
   | AExtended(_,_,(_,name,_,_,_)) -> [Printf.sprintf "@%s" name]
@@ -588,7 +588,7 @@ let assigns_hints hs froms =
   List.iter (fun ({it_content=t},_) -> term_hints hs t) froms
 
 let annot_hints hs = function
-  | AAssert(bs,ipred) | AInvariant(bs,_,ipred) ->
+  | AAssert(bs,_,ipred) | AInvariant(bs,_,ipred) ->
       List.iter (add_hint hs) (ident_names ipred.pred_name) ;
       List.iter (add_hint hs) bs
   | AAssigns(bs,Writes froms) ->
diff --git a/tests/syntax/syntactic_hook.ml b/tests/syntax/syntactic_hook.ml
index e731d80478a1ad85e8d97ee19fa17f11717eee9d..c6a5d1f3517e261599913c4c0f8f577ece146a2c 100644
--- a/tests/syntax/syntactic_hook.ml
+++ b/tests/syntax/syntactic_hook.ml
@@ -13,7 +13,7 @@ class visit = object
       [{ stmt_ghost = false;
          stmt_node =
            CODE_ANNOT(
-             AAssert([],
+             AAssert([], Assert,
                      { lexpr_node =
                          PLat ({ lexpr_node = PLtrue; lexpr_loc = loc},"Pre");
                        lexpr_loc = loc}), loc)};