diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 29bad666cec4d8aacfdbfef5c7bdee43e97f03fb..67ca47e2b299b191fe14931276ca22abae998743 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1737,14 +1737,15 @@ let step_at seq k =
 (* --- Insertion                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let in_sequence ~replace =
+let in_sequence_add_list ~replace =
   let rec in_list k h w =
     if k = 0 then
-      h :: (if replace
-            then match w with
-              | [] -> assert false
-              | _::w -> w
-            else w)
+      List.rev_append (List.rev h)
+        (if replace
+         then match w with
+           | [] -> assert false
+           | _::w -> w
+         else w)
     else
       match w with
       | [] -> assert false
@@ -1760,9 +1761,9 @@ let in_sequence ~replace =
     | Branch(p,a,b) ->
         let n = a.seq_size in
         if k < n then
-          Branch(p,in_sequence k h a,b)
+          Branch(p,in_sequence_add_list k h a,b)
         else
-          Branch(p,a,in_sequence (k-n) h b)
+          Branch(p,a,in_sequence_add_list (k-n) h b)
     | Either cs -> Either (in_case k h cs)
 
   and in_case k h = function
@@ -1770,11 +1771,13 @@ let in_sequence ~replace =
     | c::cs ->
         let n = c.seq_size in
         if k < n
-        then in_sequence k h c :: cs
+        then in_sequence_add_list k h c :: cs
         else c :: in_case (k-n) h cs
 
-  and in_sequence k h s = sequence (in_list k h s.seq_list)
-  in in_sequence
+  and in_sequence_add_list k h s = sequence (in_list k h s.seq_list)
+  in in_sequence_add_list
+
+let in_sequence ~replace id h = in_sequence_add_list ~replace id [h]
 
 let size seq = seq.seq_size
 
@@ -1791,6 +1794,12 @@ let replace ~at step sequent =
   then in_sequence ~replace:true at step seq , goal
   else raise Not_found
 
+let replace_by_step_list ~at step_list sequent =
+  let seq,goal = sequent in
+  if 0 <= at && at <= seq.seq_size
+  then in_sequence_add_list ~replace:true at step_list seq , goal
+  else raise Not_found
+
 (* -------------------------------------------------------------------------- *)
 (* --- Replace                                                            --- *)
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 9920a7c62d51da0a5685be8062930e839c835d6a..0add484d766ed51ccb96f3f481d1da388951cda3 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -153,6 +153,10 @@ val replace : at:int -> step -> sequent -> sequent
 (** replace a step in the sequent, the one [at] the specified position.
     @raise Invalid_argument if the index is out of bounds. *)
 
+val replace_by_step_list : at:int -> step list -> sequent -> sequent
+(** replace a step in the sequent, the one [at] the specified position.
+    @raise Invalid_argument if the index is out of bounds. *)
+
 val subst : (term -> term) -> sequent -> sequent
 (** Apply the atomic substitution recursively using [Lang.F.p_subst f].
     Function [f] should only transform the head of the predicate, and can assume
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index c7ae3564c95b2cbd23d5abbbca2bc60bb8d06c8f..46f3ae3cf8077927156ad9b07a006b05796503b4 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -23,6 +23,9 @@
 open Tactical
 open ProofScript
 
+let dkey_pp_allgoals =
+  Wp_parameters.register_category "script:allgoals"
+
 (* -------------------------------------------------------------------------- *)
 (* --- Alternatives Ordering                                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -389,12 +392,18 @@ let rec crawl env on_child node = function
 (* --- Main Process                                                       --- *)
 (* -------------------------------------------------------------------------- *)
 
+let pp_subgoal env fmt node =
+  let main = Env.goal env None in
+  let wpo = Env.goal env (Some node) in
+  Format.fprintf fmt "%s subgoal:@\n%a" (Wpo.get_gid main) Wpo.pp_goal_flow wpo
+
 let schedule job =
   Task.spawn (ProverTask.server ()) (Task.thread (Task.todo job))
 
 let rec process env node =
   schedule
     begin fun () ->
+      Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" (pp_subgoal env) node ;
       if ProofEngine.proved node then
         ( Env.validate env ; Task.return () )
       else
@@ -407,6 +416,7 @@ let task
     ~depth ~width ~backtrack ~auto
     ~start ~progress ~result ~success wpo =
   begin fun () ->
+    Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" Wpo.pp_goal_flow wpo ;
     Prover.simplify ~start ~result wpo >>= fun succeed ->
     if succeed
     then
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 57e324288d6ed162f81312e0e50d0a67ba4d1f74..1e20d4073b31635a76f08fe062d01ad23e966d37 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -168,32 +168,35 @@ class split =
         ~params:[]
 
     method select feedback (s : Tactical.selection) =
+      let split_cmp at title x y =
+        feedback#set_title title ;
+        feedback#set_descr
+          "Decompose into three comparisons (lt, eq, gt)" ;
+        let cases = [
+          "Lt",F.p_bool (e_lt x y);
+          "Eq",F.p_bool (e_eq x y);
+          "Gt",F.p_bool (e_lt y x);
+        ] in
+        Applicable (Tactical.insert ?at cases)
+      in
+      let split_leq at x y = split_cmp at "Split (<=)" x y in
+      let split_eq at x y = split_cmp at "Split (=)" x y in
+      let split_neq at x y = split_cmp at "Split (<>)" x y in
+      let split_lt at x y =
+        let x = if F.is_int x then F.(e_add x e_one) else x in
+        split_cmp at "Split (<)" x y
+      in
       match s with
       | Empty | Compose _ -> Not_applicable
       | Inside(_,e) ->
           begin
-            let split_cmp title x y =
-              feedback#set_title title ;
-              feedback#set_descr
-                "Decompose into three comparisons (lt, eq, gt)" ;
-              let cases = [
-                "Lt",F.p_bool (e_lt x y);
-                "Eq",F.p_bool (e_eq x y);
-                "Gt",F.p_bool (e_lt y x);
-              ] in
-              let at = Tactical.at s in
-              Applicable (Tactical.insert ?at cases)
-            in
+            let at = Tactical.at s in
             let open Qed.Logic in
             match Lang.F.repr e with
-            | Leq(x,y) -> split_cmp "Split (comp.)" x y
-            | Lt(x,y) ->
-                let x = if F.is_int x then F.(e_add x e_one) else x in
-                split_cmp "Split (comp.)" x y
-            | Eq(x,y)  when not (is_prop x || is_prop y) ->
-                split_cmp "Split (eq.)" x y
-            | Neq(x,y) when not (is_prop x || is_prop y) ->
-                split_cmp "Split (neq.)" x y
+            | Leq(x,y) -> split_leq at x y
+            | Lt(x,y) -> split_lt at x y
+            | Eq(x,y) when not (is_prop x || is_prop y) -> split_eq at x y
+            | Neq(x,y) when not (is_prop x || is_prop y) -> split_neq at x y
             | _ when F.is_prop e ->
                 feedback#set_title "Split (true,false)" ;
                 feedback#set_descr "Decompose between True and False values" ;
@@ -384,17 +387,13 @@ class split =
                       ] in
                       Applicable (Tactical.replace ~at:step.id cases)
                   | Neq(x,y) when not (is_prop x || is_prop y) ->
-                      feedback#set_title "Split (<>)";
-                      feedback#set_descr "Decompose into two comparisons (<, >)" ;
-                      let cases = ["Lt", When F.(p_bool (e_lt x y));
-                                   "Gt", When F.(p_bool (e_lt y x))] in
-                      Applicable (Tactical.replace ~at:step.id cases)
-                  | Leq(x,y) when not (is_prop x || is_prop y) ->
-                      feedback#set_title "Split (<=)";
-                      feedback#set_descr "Decompose into two comparisons (<, =)" ;
-                      let cases = ["Lt", When F.(p_bool (e_lt x y));
-                                   "Eq", When F.(p_bool (e_eq y x))] in
-                      Applicable (Tactical.replace ~at:step.id cases)
+                      split_neq (Some step.id) x y
+                  | Eq(x,y) when not (is_prop x || is_prop y) ->
+                      split_eq (Some step.id) x y
+                  | Lt(x,y) ->
+                      split_lt (Some step.id) x y
+                  | Leq(x,y) ->
+                      split_leq (Some step.id) x y
                   | If(c,p,q) ->
                       feedback#set_title "Split (if)" ;
                       feedback#set_descr "Split Conditional into Branches" ;
@@ -402,6 +401,20 @@ class split =
                       let q = F.p_bool (F.e_and [e_not c;q]) in
                       let cases = [ "Then" , When p ; "Else" , When q ] in
                       Applicable (Tactical.replace ~at:step.id cases)
+                  | And ps ->
+                      let cond p = (* keep original kind of step *)
+                        match step.condition with
+                        | Type _ -> Type p
+                        | Have _ -> Have p
+                        | When _ -> When p
+                        | Core _ -> Core p
+                        | Init _ -> Init p
+                        | _ -> assert false (* see above pattern matching *)
+                      in
+                      feedback#set_title "Split (conjunction)" ;
+                      feedback#set_descr "Split conjunction into steps" ;
+                      let ps = List.map (fun p -> cond @@ p_bool p) ps in
+                      Applicable (Tactical.replace_step ~at:step.id ps)
                   | _ ->
                       Not_applicable
                 end
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index dbc9081f0f152051df85dc8f948ecd2891e8fcd4..5fcf6a7bc0aec260d59eceab49216c724886e241 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -357,6 +357,15 @@ let replace ~at cases sequent =
        descr , Conditions.replace ~at step sequent)
     cases
 
+let replace_step ~at conditions sequent =
+  let step =
+    let s = Conditions.step_at (fst sequent) at in
+    (* keep original infos *)
+    Conditions.step ?descr:s.descr ?stmt:s.stmt ~deps:s.deps ~warn:s.warn
+  in
+  let conditions = List.map step conditions in
+  [ "Split conj", Conditions.replace_by_step_list ~at conditions sequent ]
+
 let split cases sequent =
   let hyps = fst sequent in
   List.map (fun (descr,p) -> descr,(hyps,p)) cases
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index 4ed8400c730cdca6340c68f0a0d81066f74ff61c..78159e588ce5e6cca5b7a0ccb4549e422a8f3739 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -179,6 +179,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_step : at:int -> condition list -> process
 val split : (string * pred) list -> process
 val rewrite : ?at:int -> (string * pred * term * term) list -> process
 (** For each pattern [(descr,guard,src,tgt)] replace [src] with [tgt]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1afe67759a512652f6598fedc803cf7497813d8e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -0,0 +1,707 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/split.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 23 goals scheduled
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 36) in 'test_step_branch':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    If a < b
+    Then { (* Call 'gen_P' *) Have: P_P. }
+    Else { (* Call 'gen_Q' *) Have: P_Q. }
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 46) in 'test_step_or':
+  Assume { (* Pre-condition *) Have: P_P \/ P_Q \/ P_R. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 50) in 'test_step_and':
+  Assume { (* Pre-condition *) Have: P_P /\ P_Q /\ P_R. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 54) in 'test_step_peq':
+  Assume { (* Pre-condition *) Have: L_LQ = L_LP. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 58) in 'test_step_pneq':
+  Assume { (* Pre-condition *) Have: L_LQ != L_LP. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 62) in 'test_step_neq':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: b != a.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 66) in 'test_step_leq':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: a <= b.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 70) in 'test_step_lt':
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: a < b.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 74) in 'test_step_if':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: if (a < b) then P_P else P_Q.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 78) in 'test_step_fa_if':
+  Assume {
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: forall i : Z. if (a < b) then (P_P /\ P_Pi(i)) else (P_Q /\ P_Qi(i)).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 82) in 'test_step_fa_or':
+  Assume {
+    (* Pre-condition *)
+    Have: forall i : Z. P_P \/ P_Q \/ P_R \/ P_Pi(i) \/ P_Qi(i).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 86) in 'test_step_fa_and':
+  Assume {
+    (* Pre-condition *)
+    Have: forall i : Z. P_P /\ P_Q /\ P_R /\ P_Pi(i) /\ P_Qi(i).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 90) in 'test_inside_leq':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_P /\ (a <= b).
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 94) in 'test_inside_lt':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_P /\ (a < b).
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 98) in 'test_inside_neq':
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_P /\ (b != a).
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 102) in 'test_goal_and':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_P /\ P_Q /\ P_R.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 106) in 'test_goal_eq':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: L_LQ = L_LP.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 110) in 'test_goal_neq':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: L_LQ != L_LP.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 114) in 'test_goal_if':
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_S. }
+  Prove: if (a < b) then P_P else P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 118) in 'test_goal_ex_and':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: exists i : Z. P_P /\ P_Q /\ P_Pi(i) /\ P_Qi(i).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 122) in 'test_goal_ex_or':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: exists i : Z. P_P \/ P_Q \/ P_Pi(i) \/ P_Qi(i).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 126) in 'test_goal_ex_if':
+  Assume {
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: exists i : Z. if (a < b) then (P_Pi(i) /\ P_Qi(i)) else (P_P /\ P_Q).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/split.i, line 130) in 'test_goal_ex_imply':
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: exists i : Z. (P_Q -> (P_Pi(i) -> P_Qi(i))).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_branch_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_branch_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Then *)
+    When: a < b.
+    (* Call 'gen_P' *)
+    Have: P_P.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_branch_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_branch_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_branch_ensures-1 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Else *)
+    When: b <= a.
+    (* Call 'gen_Q' *)
+    Have: P_Q.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_or_ensures-0 (generated):
+  Assume { (* Case 1/3 *) When: P_P. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_or_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_or_ensures-1 (generated):
+  Assume { (* Case 2/3 *) When: P_Q. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_or_ensures-2 (generated):
+  Assume { (* Case 3/3 *) When: P_R. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_and_ensures-0 (generated):
+  Assume {
+    (* Pre-condition *)
+    Have: P_P.
+    (* Pre-condition *)
+    Have: P_Q.
+    (* Pre-condition *)
+    Have: P_R.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_and_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_peq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_peq_ensures-0 (generated):
+  Assume { (* Both True *) When: (L_LP=true) /\ (L_LQ=true). }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_peq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_peq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_peq_ensures-1 (generated):
+  Assume { (* Both False *) When: (L_LP=false) /\ (L_LQ=false). }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_pneq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_pneq_ensures-0 (generated):
+  Assume { (* True/False *) When: (L_LQ=true) /\ (L_LP=false). }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_pneq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_pneq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_pneq_ensures-1 (generated):
+  Assume { (* False/True *) When: (L_LP=true) /\ (L_LQ=false). }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_neq_ensures-0 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Lt *) When: b < a. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_neq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_neq_ensures-1 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_neq_ensures-2 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Gt *) When: a < b. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_leq_ensures-0 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Lt *) When: a < b. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_leq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_leq_ensures-1 (generated):
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_leq_ensures-2 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_lt_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Lt *)
+    When: (2 + a) <= b.
+    (* Pre-condition *)
+    Have: a < b.
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_lt_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_lt_ensures-1 (generated):
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_lt_ensures-2 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_if_ensures-0 (generated):
+  Assume { Type: is_sint32(a) /\ is_sint32(b). (* Then *) When: P_P /\ (a < b).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_if_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_if_ensures-1 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Else *)
+    When: P_Q /\ (b <= a).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_fa_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_fa_if_ensures-0 (generated):
+  Assume {
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Then *)
+    When: P_P /\ (a < b) /\ P_Pi(i).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_fa_if_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_fa_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_fa_if_ensures-1 (generated):
+  Assume {
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Else *)
+    When: P_Q /\ (b <= a) /\ P_Qi(i).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_fa_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_fa_or_ensures-0 (generated):
+  Assume { (* Goal 1/2 *) When: forall i : Z. P_Pi(i) \/ P_Qi(i). }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_fa_or_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_step_fa_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_fa_or_ensures-1 (generated):
+  Assume { (* Goal 2/2 *) When: P_P \/ P_Q \/ P_R. }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_step_fa_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_step_fa_and_ensures-0 (generated):
+  Assume {
+    (* Split (distrib forall and) *)
+    When: P_P /\ P_Q /\ P_R /\ (forall i : Z. P_Pi(i)) /\
+        (forall i : Z. P_Qi(i)).
+  }
+  Prove: P_S.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_step_fa_and_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_inside_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_leq_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Lt *)
+    When: a < b.
+    (* Pre-condition *)
+    Have: P_P.
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_inside_leq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_inside_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_leq_ensures-1 (generated):
+  Assume { (* Pre-condition *) Have: P_P. }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_inside_leq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_leq_ensures-2 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_inside_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_lt_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Lt *)
+    When: (2 + a) <= b.
+    (* Pre-condition *)
+    Have: P_P /\ (a < b).
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_inside_lt_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_inside_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_lt_ensures-1 (generated):
+  Assume { (* Pre-condition *) Have: P_P. }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_inside_lt_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_lt_ensures-2 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_inside_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_neq_ensures-0 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Lt *)
+    When: b < a.
+    (* Pre-condition *)
+    Have: P_P.
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_inside_neq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_inside_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_neq_ensures-1 (generated):
+  Prove: true.
+  Prover Qed returns Valid
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_inside_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_inside_neq_ensures-2 (generated):
+  Assume {
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Gt *)
+    When: a < b.
+    (* Pre-condition *)
+    Have: P_P.
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_and_ensures-0 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_P.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_and_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_and_ensures-1 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_and_ensures-2 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_R.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_eq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_eq_ensures-0 (generated):
+  Assume { Have: (L_LQ=true). (* Pre-condition *) Have: P_S. }
+  Prove: (L_LP=true).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_eq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_eq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_eq_ensures-1 (generated):
+  Assume { Have: (L_LP=true). (* Pre-condition *) Have: P_S. }
+  Prove: (L_LQ=true).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_neq_ensures-0 (generated):
+  Assume { Have: (L_LQ=true). (* Pre-condition *) Have: P_S. }
+  Prove: (L_LP=false).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_neq_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_neq_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_neq_ensures-1 (generated):
+  Assume { Have: (L_LP=true). (* Pre-condition *) Have: P_S. }
+  Prove: (L_LQ=false).
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_if_ensures-0 (generated):
+  Assume {
+    Have: a < b.
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: P_P.
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_if_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_if_ensures-1 (generated):
+  Assume {
+    Have: b <= a.
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_ex_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_and_ensures-0 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_ex_and_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_ex_and_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_and_ensures-1 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_P /\ P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_ex_or_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_or_ensures-0 (generated):
+  Assume { (* Pre-condition *) Have: P_S. }
+  Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_ex_or_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_ex_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_if_ensures-0 (generated):
+  Assume {
+    Have: a < b.
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_ex_if_ensures : Unsuccess
+[wp:script:allgoals] 
+  typed_test_goal_ex_if_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_if_ensures-1 (generated):
+  Assume {
+    Have: b <= a.
+    (* Heap *)
+    Type: is_sint32(a) /\ is_sint32(b).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: P_P /\ P_Q.
+  
+  ------------------------------------------------------------
+[wp:script:allgoals] 
+  typed_test_goal_ex_imply_ensures subgoal:
+  
+  Goal Wp.Tactical.typed_test_goal_ex_imply_ensures-0 (generated):
+  Assume {
+    Have: P_Q.
+    Have: forall i : Z. P_Pi(i).
+    (* Pre-condition *)
+    Have: P_S.
+  }
+  Prove: exists i : Z. P_Qi(i).
+  
+  ------------------------------------------------------------
+[wp] [Script] Goal typed_test_goal_ex_imply_ensures : Unsuccess
+[wp] Proved goals:    0 / 23
+[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..0b28f4f1ca91c14062a0377908374d17e73d3e15
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal", "target": "P_P /\\ P_Q /\\ P_R",
+                "pattern": "&P_PP_QP_R" },
+    "children": { "Goal 1/3": [], "Goal 2/3": [], "Goal 3/3": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..f350bbe7837c4e8c6e294e015eff76da6af362e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal", "target": "L_LQ=L_LP",
+                "pattern": "=L_LQL_LP" },
+    "children": { "Necessity": [], "Sufficiency": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..34ffedfc92e639ed557ceaee33c9658797b8961c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal",
+                "target": "exists i_0:int. P_P /\\ P_Q /\\ (P_Pi i_0) /\\ (P_Qi i_0)",
+                "pattern": "\\EP_PP_Q" },
+    "children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..6f825c17e5a87b68fafd0540446281966b6b9491
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal",
+                "target": "exists i_0:int.\nif (a_0<b_0) then ((P_Pi i_0) /\\ (P_Qi i_0)) else (P_P /\\ P_Q)",
+                "pattern": "\\E<&$a$bP_PP_Q" },
+    "children": { "Then": [], "Else": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..89bbf94d5b38b9982d93a423fba7a5f9734c6e35
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal",
+                "target": "exists i_0:int. P_Q -> (P_Pi i_0) -> (P_Qi i_0)",
+                "pattern": "\\EP_Q" }, "children": { "Split": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..85f863911b0ec232b0db110410902cb0d48ee7c3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal",
+                "target": "exists i_0:int. P_P \\/ P_Q \\/ (P_Pi i_0) \\/ (P_Qi i_0)",
+                "pattern": "\\EP_PP_Q" }, "children": { "Split": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..d343a9eda31488d9af78762ddde9383029aa9250
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal",
+                "target": "if (a_0<b_0) then P_P else P_Q",
+                "pattern": "?<P_PP_Q$a$b" },
+    "children": { "Then": [], "Else": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..ab90a509a3c6d6aff740c1ced430e80b0577d8c0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-goal", "target": "L_LQ!=L_LP",
+                "pattern": "~L_LQL_LP" },
+    "children": { "Necessity": [], "Sufficiency": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..4f2228d23753d3250e95893276e846c9f2eabefe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json
@@ -0,0 +1,6 @@
+[ { "prover": "script", "verdict": "unknown" },
+  { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
+                "target": "a_0<=b_0", "pattern": "<=$a$b" },
+    "children": { "Lt": [], "Eq": [],
+                  "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..93230aab0d5ddea4b7daa1e01b1e5887af300893
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "inside-step", "at": 3, "kind": "have", "occur": 0,
+                "target": "a_0<b_0", "pattern": "<$a$b" },
+    "children": { "Lt": [], "Eq": [],
+                  "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..65ba0830f01d5ebc3027d119da6bec7115690907
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json
@@ -0,0 +1,6 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "inside-step", "at": 3, "kind": "have", "occur": 0,
+                "target": "b_0!=a_0", "pattern": "~$b$a" },
+    "children": { "Lt": [],
+                  "Eq": [ { "prover": "qed", "verdict": "valid" } ],
+                  "Gt": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..a85285d7031f7d886fc78ecc00bb8bd2415d6905
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "P_P /\\ P_Q /\\ P_R", "pattern": "&P_PP_QP_R" },
+    "children": { "Split conj": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..2e07a0b4389d4304fb36fa9eedc6dc4e491cbf02
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 3, "kind": "branch",
+                "target": "a_0<b_0", "pattern": "<$a$b" },
+    "children": { "Then": [], "Else": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_and_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_and_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..5a21b9a6c61ba869d2c65f0d6bc5c40b3bc5b1d7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_and_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "forall i_0:int. P_P /\\ P_Q /\\ P_R /\\ (P_Pi i_0) /\\ (P_Qi i_0)",
+                "pattern": "\\FP_PP_QP_R" },
+    "children": { "Split (distrib forall and)": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_if_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_if_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..43e99e4b389085ba5f4cb3e3cea4bbce41e47937
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_if_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 2, "kind": "have",
+                "target": "forall i_0:int.\nif (a_0<b_0) then (P_P /\\ (P_Pi i_0)) else (P_Q /\\ (P_Qi i_0))",
+                "pattern": "\\F<$a$bP_PP_Q" },
+    "children": { "Then": [], "Else": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_or_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_or_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..bd1a0deb16416d21f29bd5f588052c2d95d4205d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_fa_or_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "forall i_0:int. P_P \\/ P_Q \\/ P_R \\/ (P_Pi i_0) \\/ (P_Qi i_0)",
+                "pattern": "\\FP_PP_QP_R" },
+    "children": { "Goal 1/2": [], "Goal 2/2": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_if_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_if_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..d490f51fad0ea33cf3db678f27d46a7c95825591
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_if_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 2, "kind": "have",
+                "target": "if (a_0<b_0) then P_P else P_Q",
+                "pattern": "?<P_PP_Q$a$b" },
+    "children": { "Then": [], "Else": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..cb1d6260cf6a597c14203c7472f4d1be45a07ef2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_leq_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 2, "kind": "have",
+                "target": "a_0<=b_0", "pattern": "<=$a$b" },
+    "children": { "Lt": [], "Eq": [],
+                  "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..4347aa1946c8d615ebf0ba21139395638c4d1bef
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_lt_ensures.json
@@ -0,0 +1,5 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 2, "kind": "have",
+                "target": "a_0<b_0", "pattern": "<$a$b" },
+    "children": { "Lt": [], "Eq": [],
+                  "Gt": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..8c70aaa2bdeb00c6e9a595aa761fa1580f3d0725
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_neq_ensures.json
@@ -0,0 +1,6 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 2, "kind": "have",
+                "target": "b_0!=a_0", "pattern": "~$b$a" },
+    "children": { "Lt": [],
+                  "Eq": [ { "prover": "qed", "verdict": "valid" } ],
+                  "Gt": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_or_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_or_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..16028f0fe86eb40dff2f5ceb73bbfb937fdabbfb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_or_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "P_P \\/ P_Q \\/ P_R", "pattern": "|P_PP_QP_R" },
+    "children": { "Case 1/3": [], "Case 2/3": [], "Case 3/3": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..757220f3f5af8c70ad6ac9c81b48d74a05c9ce39
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_peq_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "L_LQ=L_LP", "pattern": "=L_LQL_LP" },
+    "children": { "Both True": [], "Both False": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json
new file mode 100644
index 0000000000000000000000000000000000000000..d57b97bec5d685d7488355c13124afcb50562bd8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_pneq_ensures.json
@@ -0,0 +1,4 @@
+[ { "header": "Split", "tactic": "Wp.split", "params": {},
+    "select": { "select": "clause-step", "at": 1, "kind": "have",
+                "target": "L_LQ!=L_LP", "pattern": "~L_LQL_LP" },
+    "children": { "True/False": [], "False/True": [] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i
new file mode 100644
index 0000000000000000000000000000000000000000..6aff2d20b8542b319d535c902053171c3ad83ed6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/split.i
@@ -0,0 +1,131 @@
+/* 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
+*/
+/* run.config_qualif
+   DONTRUN:
+*/
+
+/*@ axiomatic X {
+      predicate P ;
+      predicate Q ;
+      predicate R ;
+      predicate S ;
+
+      predicate Pi (integer x);
+      predicate Qi (integer x);
+
+      logic boolean LP ;
+      logic boolean LQ ;
+    }
+*/
+
+int a, b;
+
+/*@ assigns \nothing;
+  @ ensures P ; */
+void gen_P(void);
+
+/*@ assigns \nothing;
+  @ ensures Q ; */
+void gen_Q(void);
+
+/*@ assigns \nothing;
+  @ ensures R ; */
+void gen_R(void);
+
+//@ ensures S ;
+void test_step_branch(void) {
+  if (a < b) {
+    gen_P();
+  } else {
+    gen_Q();
+  }
+}
+
+/*@ requires P || Q || R ;
+  @ ensures S ; */
+void test_step_or(void) {}
+
+/*@ requires P && Q && R ;
+  @ ensures S ; */
+void test_step_and(void) {}
+
+/*@ requires LP == LQ ;
+  @ ensures S ; */
+void test_step_peq(void) {}
+
+/*@ requires LP != LQ ;
+  @ ensures S ; */
+void test_step_pneq(void) {}
+
+/*@ requires a != b ;
+  @ ensures S ; */
+void test_step_neq(void) {}
+
+/*@ requires a <= b ;
+  @ ensures S ; */
+void test_step_leq(void) {}
+
+/*@ requires a < b ;
+  @ ensures S ; */
+void test_step_lt(void) {}
+
+/*@ requires (a < b) ? P : Q ;
+  @ ensures S ; */
+void test_step_if(void) {}
+
+/*@ requires \forall integer i ; (a < b) ? P && Pi(i) : Q && Qi(i) ;
+  @ ensures S ; */
+void test_step_fa_if(void) {}
+
+/*@ requires \forall integer i ; Pi(i) || P || Qi(i) || Q || R ;
+  @ ensures S ; */
+void test_step_fa_or(void) {}
+
+/*@ requires \forall integer i ; Pi(i) && P && Qi(i) && Q && R ;
+  @ ensures S ; */
+void test_step_fa_and(void) {}
+
+/*@ requires P && a <= b ;
+  @ ensures Q ; */
+void test_inside_leq(void) {}
+
+/*@ requires P && a < b ;
+  @ ensures Q ; */
+void test_inside_lt(void) {}
+
+/*@ requires P && a != b ;
+  @ ensures Q ; */
+void test_inside_neq(void) {}
+
+/*@ requires S ;
+  @ ensures P && Q && R ; */
+void test_goal_and(void) {}
+
+/*@ requires S ;
+  @ ensures LP == LQ ; */
+void test_goal_eq(void) {}
+
+/*@ requires S ;
+  @ ensures LP != LQ ; */
+void test_goal_neq(void) {}
+
+/*@ requires S ;
+  @ ensures (a < b) ? P : Q ; */
+void test_goal_if(void) {}
+
+/*@ requires S ;
+  @ ensures \exists integer i ; P && Q && Pi(i) && Qi(i) ; */
+void test_goal_ex_and(void) {}
+
+/*@ requires S ;
+  @ ensures \exists integer i ; P || Q || Pi(i) || Qi(i) ; */
+void test_goal_ex_or(void) {}
+
+/*@ requires S ;
+  @ ensures \exists integer i ; (a < b) ? Pi(i) && Qi(i) : P && Q ; */
+void test_goal_ex_if(void) {}
+
+/*@ requires S ;
+  @ ensures \exists integer i ; Pi(i) && Q ==> Qi(i); */
+void test_goal_ex_imply(void) {}