diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index e281a3b8920dd3e5aeb7273af369d2d90866d9e0..49ffb79f66f68216a4917a8bae7187ca1341984e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3774,21 +3774,24 @@ struct
     append_loop_labels (append_here_label (append_pre_label (append_init_label
                                                                (Lenv.empty()))))
 
+  let assertion_kind =
+    function Assert -> Cil_types.Assert | Check -> Cil_types.Check
+
   let code_annot loc current_behaviors current_return_type ca =
     let source = fst loc in
     let annot = match ca with
-      | AAssert (behav,Assert,p) ->
-        check_behavior_names loc current_behaviors behav;
-        Cil_types.AAssert (behav, Cil_types.Assert, predicate (code_annot_env()) p)
-      | AAssert (behav,Check,p) ->
+      | AAssert (behav,k,p) ->
         check_behavior_names loc current_behaviors behav;
-        Cil_types.AAssert (behav, Cil_types.Check, predicate (code_annot_env()) p)
+        Cil_types.AAssert(behav,assertion_kind k,predicate (code_annot_env()) p)
       | APragma (Impact_pragma sp) ->
-        Cil_types.APragma (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
+        Cil_types.APragma
+          (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
       | APragma (Slice_pragma sp) ->
-        Cil_types.APragma (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
+        Cil_types.APragma
+          (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
       | APragma (Loop_pragma lp) ->
-        Cil_types.APragma (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
+        Cil_types.APragma
+          (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
       | AStmtSpec (behav,s) ->
         (* function behaviors and statement behaviors are not at the
            same level. Do not mix them in a complete or disjoint clause