diff --git a/convert_acsl.ml b/convert_acsl.ml
index 82c53f05fb713bb9edf411e1a6b813d769adf0b6..d176166483eaa0a976c63157bd0b0ba964befab5 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -594,9 +594,9 @@ let convert_assigns env = function
       Logic_ptree.Writes (List.map (convert_from env) l)
 
 let convert_pred_tp env p =
-  (* TODO: support check in ACSL++. *)
+  (* TODO: support check and admit in ACSL++. *)
   let tp_statement = convert_pred_named env p in
-  { tp_only_check = false; tp_statement }
+  { tp_kind = Assert; tp_statement }
 
 let convert_termination_kind = function
   | Intermediate_format.Normal -> Cil_types.Normal
diff --git a/generate_spec.ml b/generate_spec.ml
index 93f48b10e4c88f985de9d846f7185facf72f1dec..a18b5560446244eb7b1bb2c9f95716961b8eeb27 100644
--- a/generate_spec.ml
+++ b/generate_spec.ml
@@ -23,7 +23,7 @@
 open Logic_ptree
 open Intermediate_format
 
-let toplevel_pred tp_statement = { tp_only_check = false; tp_statement }
+let toplevel_pred tp_statement = { tp_kind = Assert; tp_statement }
 
 let const_valid lexpr_loc pkind t =
   let lexpr_node =