diff --git a/src/plugins/wp/GuiSequent.ml b/src/plugins/wp/GuiSequent.ml
index fdb29988b39ecae1b81bc3f91b8cd17ccadb008c..aaf112abc48264d254f3062d2d58f0d3291732d8 100644
--- a/src/plugins/wp/GuiSequent.ml
+++ b/src/plugins/wp/GuiSequent.ml
@@ -623,7 +623,7 @@ class focused (wtext : Wtext.text) =
 
     method set_target tgt =
       match tgt with
-      | Tactical.Empty | Tactical.Compose _ ->
+      | Tactical.Empty | Tactical.Compose _ | Tactical.Multi _ ->
           begin
             pcond#set_target Term ;
             plang#clear_target ;
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 3e0bcc83cc2e0545b379335b14211c9397578161..531175ba1eec83466e6fb7d5df905a926b41a4af 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -97,6 +97,7 @@ let j_step = j_select "clause-step"
 let j_ingoal = j_select "inside-goal"
 let j_instep = j_select "inside-step"
 let j_compose = j_select "compose"
+let j_multi = j_select "multi"
 let j_kint = j_select "kint"
 let j_range = j_select "range"
 let j_id a = "id" , `String a
@@ -136,6 +137,9 @@ let rec json_of_selection = function
       `Assoc [ j_instep ; j_at s ; j_kind s ; j_occur n ;
                j_term e ; j_pattern m ]
 
+  | Multi es ->
+      `Assoc (j_multi :: j_args es)
+
 and j_args = function
   | [] -> []
   | es -> ["args" , `List (List.map json_of_selection es)]
@@ -184,6 +188,9 @@ let rec selection_of_json ((hs,g) as s : sequent) js =
         let id = j_id js in
         let args = j_args js in
         Tactical.compose id (List.map (selection_of_json s) args)
+    | "multi" ->
+        let args = j_args js in
+        Tactical.multi @@ List.map (selection_of_json s) args
     | "kint" -> Tactical.cint (j_val js)
     | "range" -> Tactical.range (j_min js) (j_max js)
     | _ -> raise Not_found
diff --git a/src/plugins/wp/TacChoice.ml b/src/plugins/wp/TacChoice.ml
index 31f3ee05e0cd795e8b57e1464b04e44906b3416e..28ba26f16aed2a59c62767c2ce30958d782fd219 100644
--- a/src/plugins/wp/TacChoice.ml
+++ b/src/plugins/wp/TacChoice.ml
@@ -45,7 +45,7 @@ class choice =
                 Applicable (fun (hs,_) -> ["Choice",(hs,F.p_bool q)])
             | _ -> Not_applicable
           end
-      | Empty | Compose _ | Clause _ | Inside(Step _,_) ->
+      | Empty | Compose _ | Clause _ | Inside(Step _,_) | Multi _ ->
           Not_applicable
   end
 
@@ -59,7 +59,7 @@ class absurd =
 
     method select _feedback (s : Tactical.selection) =
       match s with
-      | Empty | Compose _ | Inside _ | Clause(Goal _)
+      | Empty | Compose _ | Inside _ | Clause(Goal _) | Multi _
         -> Not_applicable
       | Clause(Step s) ->
           begin
@@ -85,7 +85,7 @@ class contrapose =
 
     method select _feedback (s : Tactical.selection) =
       match s with
-      | Empty | Compose _ | Inside _ | Clause(Goal _)
+      | Empty | Compose _ | Inside _ | Clause(Goal _) | Multi _
         -> Not_applicable
       | Clause(Step s) ->
           begin
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 62492909112d90a938b3be35e092e682a0a44e40..73f33b2e8cfbbac93770098b6c48f349f1013dc7 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -21,6 +21,59 @@
 (**************************************************************************)
 
 open Tactical
+open Conditions
+
+let condition original p = (* keep original kind of simple condition *)
+  match original.condition with
+  | Type _ -> Type p
+  | Have _ -> Have p
+  | When _ -> When p
+  | Core _ -> Core p
+  | Init _ -> Init p
+  | _ -> assert false
+
+let tactical_step step =
+  Tactical.replace_single ~at:step.id ("Removed", Conditions.Have Lang.F.p_true)
+
+module TermLset = Qed.Listset.Make(Lang.F.QED.Term)
+
+let tactical_inside step remove =
+  let remove = List.sort_uniq Lang.F.compare remove in
+  let collect p =
+    match Lang.F.p_expr p with
+    | And ps -> ps
+    | _ -> [ p ]
+  in
+  begin match step.condition with
+    | Type p | Have p | When p | Core p | Init p ->
+        let ps = Lang.F.e_props @@ collect p in
+        let ps = TermLset.diff ps remove in
+        let cond = condition step @@ Lang.F.p_bool @@ Lang.F.e_and ps in
+        Tactical.replace_single ~at:step.id ("Filtered", cond)
+
+    | _ -> raise Not_found
+  end
+
+module Smap = Qed.Idxmap.Make
+    (struct
+      type t = step
+      let id s = s.id
+    end)
+
+let collect_remove m = function
+  | Inside(Step step, remove) ->
+      let l =
+        try Smap.find step m
+        with Not_found -> []
+      in
+      Smap.add step (remove :: l) m
+  | _ -> raise Not_found
+
+let fold_selection s seq =
+  let m = List.fold_left collect_remove Smap.empty s in
+  "Filtered", Smap.fold (fun s l seq -> snd @@ tactical_inside s l seq) m seq
+
+let process (f: sequent -> string * sequent) s = [ f s ]
 
 class clear =
   object(_)
@@ -32,10 +85,15 @@ class clear =
     method select _feedback sel =
       match sel with
       | Clause(Step step) ->
-          let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
-          Applicable (Tactical.replace ~at:step.id removed)
-      | _ ->
-          Not_applicable
+          Applicable(process @@ tactical_step step)
+      | Inside(Step step, remove) ->
+          begin
+            try Applicable(process @@ tactical_inside step [remove])
+            with Not_found -> Not_applicable
+          end
+      | Multi es ->
+          Applicable (process @@ fold_selection es)
+      | _ -> Not_applicable
   end
 
 let tactical = Tactical.export (new clear)
diff --git a/src/plugins/wp/TacCompound.ml b/src/plugins/wp/TacCompound.ml
index e4fe08b7833af851cf7445e259c0b8f33d092c46..53c984d681cfecf23fc3cf4d69f7318e37b59544 100644
--- a/src/plugins/wp/TacCompound.ml
+++ b/src/plugins/wp/TacCompound.ml
@@ -209,7 +209,7 @@ class compound =
         | Clause (Step s) -> process_have feedback s
         | Clause (Goal p) -> process_goal feedback p
         | Inside(_,e) -> process_expand feedback ?at:(Tactical.at s) e
-        | Empty | Compose _ -> raise Not_found
+        | Empty | Compose _ | Multi _ -> raise Not_found
       in Applicable process
 
   end
diff --git a/src/plugins/wp/TacNormalForm.ml b/src/plugins/wp/TacNormalForm.ml
index f7e78a439060a170bec100c699899079258360b4..a3ca166d4d31e5b3cb6d4270a67f56d0a6ae19a9 100644
--- a/src/plugins/wp/TacNormalForm.ml
+++ b/src/plugins/wp/TacNormalForm.ml
@@ -73,7 +73,7 @@ let match_selection = function
             else Some (false, e, f_nf_hyp s e)
         | _ -> None
       end
-  | Inside(_,_) | Compose _ | Empty -> None
+  | Inside(_,_) | Compose _ | Empty | Multi _ -> None
 
 class normal_form =
   object
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 1e20d4073b31635a76f08fe062d01ad23e966d37..20857de0be03c63f38eaaf97c345129968666858 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -187,7 +187,7 @@ class split =
         split_cmp at "Split (<)" x y
       in
       match s with
-      | Empty | Compose _ -> Not_applicable
+      | Empty | Compose _ | Multi _ -> Not_applicable
       | Inside(_,e) ->
           begin
             let at = Tactical.at s in
diff --git a/src/plugins/wp/TacUnfold.ml b/src/plugins/wp/TacUnfold.ml
index fd4f9e3a3b9ef8abe8f678b03fc1c98c42e598d4..e64bfec45f97b0c11f2004a0050c429fc77fc090 100644
--- a/src/plugins/wp/TacUnfold.ml
+++ b/src/plugins/wp/TacUnfold.ml
@@ -22,6 +22,7 @@
 
 open Lang
 open Tactical
+open Conditions
 
 (* -------------------------------------------------------------------------- *)
 (* --- Unfold Definition Tactical                                         --- *)
@@ -48,6 +49,8 @@ let range f es =
       (F.p_leq e (F.e_zint b)) in
   F.e_prop (F.p_all range es)
 
+(* Used only for non Multi selection *)
+
 let rec applicable ?at e f es = function
   | phi::others ->
       begin
@@ -61,6 +64,82 @@ let rec applicable ?at e f es = function
   | [] ->
       Not_applicable
 
+(* Used only for Multi selection *)
+
+module Smap = Qed.Idxmap.Make
+    (struct
+      type t = step
+      let id s = s.id
+    end)
+
+let condition original p = (* keep original kind of simple condition *)
+  match original.condition with
+  | Type _ -> Type p
+  | Have _ -> Have p
+  | When _ -> When p
+  | Core _ -> Core p
+  | Init _ -> Init p
+  | _ -> assert false
+
+let collect_term_to_unfold (g, m) = function
+  | Inside(Step step, unfold) ->
+      let l =
+        try Smap.find step m
+        with Not_found -> []
+      in
+      g, Smap.add step (unfold :: l) m
+  | Inside (Goal _, unfold) ->
+      begin match g with
+        | None -> Some [ unfold ], m
+        | Some g -> Some (unfold :: g), m
+      end
+  | _ -> raise Not_found
+
+let rec collect_unfold phis m e =
+  match phis with
+  | phi :: others ->
+      begin
+        try
+          match F.repr e with
+          | Qed.Logic.Fun(f,es) -> Lang.F.Tmap.add e (phi f es) m
+          | _ -> raise Not_found
+        with Not_found | Invalid_argument _ -> collect_unfold others m e
+      end
+  | [] -> m
+
+let unfolds_from_list phis es =
+  List.fold_left (collect_unfold phis) Lang.F.Tmap.empty es
+
+let unfolds_from_smap phis m =
+  Smap.map (fun _s es -> unfolds_from_list phis es) m
+
+let tactical_inside step unfolds sequent =
+  if Lang.F.Tmap.is_empty unfolds
+  then raise Not_found
+  else match step.condition with
+    | Type p | Have p | When p | Core p | Init p ->
+        let subst t = Lang.F.Tmap.find t unfolds in
+        let p = condition step @@ Lang.p_subst subst p in
+        snd @@ Tactical.replace_single ~at:step.id ("Unfolded", p) sequent
+    | _ -> raise Not_found
+
+let tactical_goal unfolds (seq, g) =
+  if Lang.F.Tmap.is_empty unfolds
+  then raise Not_found
+  else
+    let subst t = Lang.F.Tmap.find t unfolds in
+    seq, Lang.p_subst subst g
+
+let fold_selection goal_unfolds step_unfolds sequent =
+  "Unfolded multiple selection",
+  let add_goal = match goal_unfolds with
+    | None -> Extlib.id
+    | Some goal_unfolds -> tactical_goal goal_unfolds
+  in
+  add_goal @@ Smap.fold tactical_inside step_unfolds sequent
+
+let process (f: sequent -> string * sequent) s = [ f s ]
+
 class unfold =
   object
     inherit Tactical.make ~id:"Wp.unfold"
@@ -69,13 +148,21 @@ class unfold =
         ~params:[]
 
     method select _feedback (s : Tactical.selection) =
-      let at = Tactical.at s in
-      let e = Tactical.selected s in
-      match F.repr e with
-      | Qed.Logic.Fun(f,es) ->
-          applicable ?at e f es [ definition ; range ]
-      | _ -> Not_applicable
-
+      let unfoldings = [ definition ; range ] in
+      match s with
+      | Multi es ->
+          let goal, steps =
+            List.fold_left collect_term_to_unfold (None, Smap.empty) es in
+          let goal = Option.map (unfolds_from_list unfoldings) goal in
+          let steps = unfolds_from_smap unfoldings steps in
+          Applicable (process @@ fold_selection goal steps)
+      | s ->
+          let at = Tactical.at s in
+          let e = Tactical.selected s in
+          match F.repr e with
+          | Qed.Logic.Fun(f,es) ->
+              applicable ?at e f es unfoldings
+          | _ -> Not_applicable
   end
 
 let tactical = Tactical.export (new unfold)
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 5fcf6a7bc0aec260d59eceab49216c724886e241..1da597fa8d3801f73d9ccea94c08f929a52f5d03 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -79,6 +79,7 @@ type selection =
   | Clause of clause
   | Inside of clause * term
   | Compose of compose
+  | Multi of selection list
 
 and compose =
   | Cint of Integer.t
@@ -105,6 +106,7 @@ let selected = function
   | Inside(_,t) -> t
   | Clause c -> e_prop (head c)
   | Compose code -> composed code
+  | Multi _s -> e_true (* For now, do not provide this *)
 
 let get_int_z z =
   try Some (Integer.to_int_exn z) with Z.Overflow -> None
@@ -148,6 +150,10 @@ let rec pp_selection fmt = function
       Format.fprintf fmt "@[<hov 2>Compose '%s'" id ;
       List.iter (fun e -> Format.fprintf fmt "(%a)" pp_selection e) es ;
       Format.fprintf fmt "@]"
+  | Multi es ->
+      Format.fprintf fmt "@[<hov 2>Multi-selection" ;
+      List.iter (fun e -> Format.fprintf fmt "(%a)" pp_selection e) es ;
+      Format.fprintf fmt "@]"
 
 let int a = Compose(Cint (Integer.of_int a))
 let cint a = Compose(Cint a)
@@ -161,6 +167,8 @@ let compose id es =
     | _ -> Compose(Code(e,id,es))
   with Not_found -> Empty
 
+let multi es = Multi es
+
 let findhead (s:selection) e =
   match s with
   | Empty -> None
@@ -172,6 +180,7 @@ let findhead (s:selection) e =
       else None
   | Compose(Code(v,_,_)) as s ->
       if v == e then Some s else None
+  | Multi _ -> None
 
 let rec lookup (s:selection) e q =
   match findhead s e with
@@ -334,7 +343,7 @@ class type feedback =
 (* -------------------------------------------------------------------------- *)
 
 let at = function
-  | Empty | Clause (Goal _) | Inside(Goal _,_) | Compose _ -> None
+  | Empty | Clause (Goal _) | Inside(Goal _,_) | Compose _ | Multi _ -> None
   | Clause (Step s) | Inside(Step s,_) -> Some s.id
 
 let mapi f cases =
@@ -357,6 +366,10 @@ let replace ~at cases sequent =
        descr , Conditions.replace ~at step sequent)
     cases
 
+let replace_single ~at (descr,cond) sequent =
+  let step = Conditions.(step ~descr cond) in
+  descr , Conditions.replace ~at step sequent
+
 let replace_step ~at conditions sequent =
   let step =
     let s = Conditions.step_at (fst sequent) at in
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index 78159e588ce5e6cca5b7a0ccb4549e422a8f3739..f7ea9130bf0abf129ce56511608662878bdcbd4f 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -41,6 +41,7 @@ type selection =
   | Clause of clause
   | Inside of clause * term
   | Compose of compose
+  | Multi of selection list
 
 and compose = private
   | Cint of Integer.t
@@ -51,6 +52,7 @@ val int : int -> selection
 val cint : Integer.t -> selection
 val range : int -> int -> selection
 val compose : string -> selection list -> selection
+val multi : selection list -> selection
 val get_int : selection -> int option
 val destruct : selection -> selection list
 
@@ -179,6 +181,7 @@ val at : selection -> int option
 val mapi : (int -> int -> 'a -> 'b) -> 'a list -> 'b list
 val insert : ?at:int -> (string * pred) list -> process
 val replace : at:int -> (string * condition) list -> process
+val replace_single : at:int -> string * condition -> sequent -> string * sequent
 val replace_step : at:int -> condition list -> process
 val split : (string * pred) list -> process
 val rewrite : ?at:int -> (string * pred * term * term) list -> process
diff --git a/src/plugins/wp/tests/wp_tip/TacNOP.ml b/src/plugins/wp/tests/wp_tip/TacNOP.ml
index 7b2413cd0a66588084c5df65be5ec6f34b468e9d..a398efe3ac597d6d3b7dec5ff98f1d206c299f59 100644
--- a/src/plugins/wp/tests/wp_tip/TacNOP.ml
+++ b/src/plugins/wp/tests/wp_tip/TacNOP.ml
@@ -16,6 +16,7 @@ class nop =
       match s with
       | Empty -> Not_applicable
       | Compose _
+      | Multi _
       | Inside _
       | Clause _ ->
           feedback#set_title "NOP" ;
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
index 6abddf24da825c3c378e921cb3f540f9b7b18a78..38bb4997fe998982b6335db4dcbcc26d541cd45e 100644
--- a/src/plugins/wp/tests/wp_tip/clear.i
+++ b/src/plugins/wp/tests/wp_tip/clear.i
@@ -1,5 +1,5 @@
 /* run.config
-   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/oracle/@PTEST_NAME@.session
+   OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
 */
 /* run.config_qualif
    DONTRUN:
@@ -26,3 +26,8 @@ void clear(void) {
     b--;
   }
 }
+
+void clear_in_step(void){
+  //@ admit P && Q && R ;
+  //@ check S(42) ;
+}
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index 72226ceb96e8ff55db312aa84e551ba12fb48bd8..85363bf27b51a638d6c2a5287d6a1f7a50e80470 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -2,7 +2,147 @@
 [kernel] Parsing clear.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
-[wp] [Failed] Goal typed_clear_ensures
-[wp] Proved goals:    0 / 1
+[wp] 2 goals scheduled
+[wp:script:allgoals] 
+  Goal Post-condition (file clear.i, line 21) in 'clear':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    (* Pre-condition *)
+    Have: P_R.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). Have: (1 + a_1) = a. }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Check (file clear.i, line 32):
+  Assume { (* Admit *) Have: P_P /\ P_Q /\ P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    (* Pre-condition *)
+    Have: P_R.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
+  Assume { (* Filtered *) Have: P_Q /\ P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-1 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1) /\ is_sint32(b_2).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    If a_2 < b_2
+    Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+    Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
+  Assume { (* Filtered *) Have: P_R. }
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-2 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+        is_sint32(b_1).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    If a_2 < b_1
+    Then { Have: (a_2 = a_1) /\ (b_1 = b). }
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_in_step_check subgoal:
+  
+  Goal Wp.Tactical.typed_clear_in_step_check-2 (generated):
+  Prove: P_S(42).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_in_step_check : Unsuccess
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-3 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+  }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-4 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_P. }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-5 (generated):
+  Assume { (* Pre-condition *) Have: P_P. }
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_clear_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_clear_ensures-6 (generated):
+  Prove: P_S(a + b).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_ensures : Unsuccess
+[wp] Proved goals:    0 / 2
 [wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
new file mode 100644
index 0000000000000000000000000000000000000000..231674bdd87b18979b9942eb2b9d72272ff0a590
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
@@ -0,0 +1,20 @@
+[ { "header": "Clear", "tactic": "Wp.clear", "params": {},
+    "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
+                "target": "P_P", "pattern": "P_P" },
+    "children": { "Filtered": [ { "header": "Clear", "tactic": "Wp.clear",
+                                  "params": {},
+                                  "select": { "select": "inside-step",
+                                              "at": 2, "kind": "have",
+                                              "occur": 0, "target": "P_Q",
+                                              "pattern": "P_Q" },
+                                  "children": { "Filtered": [ { "header": "Clear",
+                                                                "tactic": "Wp.clear",
+                                                                "params": {},
+                                                                "select": 
+                                                                  { "select": "clause-step",
+                                                                    "at": 2,
+                                                                    "kind": "have",
+                                                                    "target": "P_R",
+                                                                    "pattern": "P_R" },
+                                                                "children": 
+                                                                  { "Cleared hypothesis": [] } } ] } } ] } } ]