diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index b283054819553df4d0046b32ef3c7e8774123ea9..3a0b67f0857f54158c41ba96b0974678e1683240 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -108,24 +108,33 @@ let term_lvals_of_term t =
 let behavior_assumes b =
   Logic_const.pands (List.map Logic_const.pred_of_id_pred b.b_assumes)
 
-let behavior_postcondition b k =
+let take_ip ~goal (ip : identified_predicate) =
+  let { tp_kind ; tp_statement } = ip.ip_content in
+  let take_it =
+    if goal
+    then Logic_utils.verify_predicate tp_kind
+    else Logic_utils.use_predicate tp_kind in
+  if take_it then tp_statement else Logic_const.ptrue
+
+let behavior_postcondition ~goal b k =
   let assumes = Logic_const.pold (behavior_assumes b) in
   let postcondition =
     Logic_const.pands
-      (Extlib.filter_map (fun (x,_) -> x = k)
-         (Extlib.($) Logic_const.pred_of_id_pred snd) b.b_post_cond)
-  in
-  Logic_const.pimplies (assumes,postcondition)
+      (List.map
+         (fun (tk,ip) ->
+            if tk = k then take_ip ~goal ip else Logic_const.ptrue)
+         b.b_post_cond)
+  in Logic_const.pimplies (assumes,postcondition)
 
-let behavior_precondition b =
+let behavior_precondition ~goal b =
   let assumes = behavior_assumes b in
-  let requires = Logic_const.pands
-      (List.rev_map Logic_const.pred_of_id_pred b.b_requires)
-  in
-  Logic_const.pimplies (assumes,requires)
+  let requires =
+    Logic_const.pands
+      (List.map (take_ip ~goal) b.b_requires)
+  in Logic_const.pimplies (assumes,requires)
 
-let precondition spec =
-  Logic_const.pands (List.map behavior_precondition spec.spec_behavior)
+let precondition ~goal spec =
+  Logic_const.pands (List.map (behavior_precondition ~goal) spec.spec_behavior)
 
 (** find the behavior named [name] in the list *)
 let get_named_bhv bhv_list name =
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index 22cef1f703033543f59da7d347470cd9e330fa71..83ac664e106bea47a39161ede6bc926b05e476c3 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -65,21 +65,32 @@ val term_lvals_of_term: term -> term_lval list
 (** @return the list of all the term lvals of a given term.
     Purely syntactic function. *)
 
-val precondition : funspec -> predicate
+val precondition : goal:bool -> funspec -> predicate
 (** Builds the precondition from [b_assumes] and [b_requires] clauses.
-    @since Carbon-20101201 *)
+    With [~goal:true], only returns assert and check predicates.
+    With [~goal:false], only returns assert and admit predicates.
+    @since Carbon-20101201
+    @modify Frama-C+dev introduce [goal] flag
+*)
 
 val behavior_assumes : funbehavior -> predicate
 (** Builds the conjunction of the [b_assumes].
     @since Nitrogen-20111001 *)
 
-val behavior_precondition : funbehavior -> predicate
+val behavior_precondition : goal:bool -> funbehavior -> predicate
 (** Builds the precondition from [b_assumes] and [b_requires] clauses.
-    @since Carbon-20101201 *)
+    For flag [~goal] see {!Ast_info.precondition} above.
+    @since Carbon-20101201
+    @modify Frama-C+dev introduce [goal] flag
+*)
 
-val behavior_postcondition : funbehavior -> termination_kind -> predicate
+val behavior_postcondition :
+  goal:bool -> funbehavior -> termination_kind -> predicate
 (** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
-    @modify Boron-20100401 added termination kind as filtering argument. *)
+    For flag [~goal] see {Ast_info.precondition} above.
+    @modify Boron-20100401 added termination kind as filtering argument.
+    @modify Frama-C+dev introduce [goal] flag
+*)
 
 val disjoint_behaviors : funspec -> string list -> predicate
 (** Builds the [disjoint_behaviors] property for the behavior names.
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 80ffaf64513064f8ffcb5b9c9ae1d41f6343f2da..681da07c72e82ee75b37b126bd068b862f0a0a2b 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -150,15 +150,15 @@ exception CannotMerge of string
    [merge_object path json_obj] recursively merges the object [json_obj] into the
    JSON file [path]. If [path] does not exist, it is created.
    Merge consists in combining values with the same key, e.g. if [path]
-   already contains an object {"kernel": {"options": ["a"]}}, and
-   [json_obj] is {"kernel": {"options": ["b"]}}, the result will be
-   {"kernel": {"options": ["a", "b"]}}. Cannot merge heterogeneous
+   already contains an object [{"kernel": {"options": ["a"]}}], and
+   [json_obj] is [{"kernel": {"options": ["b"]}}], the result will be
+   [{"kernel": {"options": ["a", "b"]}}]. Cannot merge heterogeneous
    objects, i.e. in the previous example, if "options" were associated
    with a string in [path], trying to merge an array into it would
-   raise [JsonCannotMerge].
+   raise [CannotMerge].
    The merged object is updated in the memory cache.
 
-   @raise [CannotMerge] if the objects have conflicting types for
+   @raise CannotMerge if the objects have conflicting types for
    the same keys, or if the root JSON element is not an object.
    @since Frama-C+dev
 *)
@@ -170,7 +170,7 @@ val merge_object : Filepath.Normalized.t -> Yojson.Basic.t -> unit
    Unlike objects, arrays are merged by simply concatenating their list
    of elements.
 
-   @raise [CannotMerge] if the root JSON element is not an array.
+   @raise CannotMerge if the root JSON element is not an array.
    @since Frama-C+dev
 *)
 val merge_array : Filepath.Normalized.t -> Yojson.Basic.t -> unit