diff --git a/src/plugins/wp/Pattern.ml b/src/plugins/wp/Pattern.ml
index c0660c931eb529f218cdeb03ab8c3efdefd1d641..35022166319bd93bfcc7b71abb650a168c605315 100644
--- a/src/plugins/wp/Pattern.ml
+++ b/src/plugins/wp/Pattern.ml
@@ -423,11 +423,9 @@ and ptry env p e =
and pany env op rs es =
match rs , es with
| [] , [] -> ()
- | rs , [] ->
- let e = op [] in
- List.iter (fun r -> pmatch env r e) rs
+ | [] , _ | _ , [] -> raise Not_found
+ | [r] , _ -> pmatch env r (op es)
| r::rs , e::es -> pmatch env r e ; pany env op rs es
- | [] , _::_ -> raise Not_found
(* Pairwise matching *)
and pargs env ps trail es =
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/pac.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/pac.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..49efe1a3da3631597d500e68e61bc5f93786e3dc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/pac.res.oracle
@@ -0,0 +1,143 @@
+# frama-c -wp [...]
+[kernel] Parsing pac.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal target3_no_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target3_no_match_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal target4_exact_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target4_exact_match_terminates (Cfg) (Trivial)
+[wp] [Valid] Goal target5_extra_match_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal target5_extra_match_terminates (Cfg) (Trivial)
+[wp] 6 goals scheduled
+[wp] [NoResult] typed_target3_no_match_ensures_post (Qed)
+[wp] [Valid] typed_target3_no_match_assigns (Qed)
+[wp] [Valid] typed_target4_exact_match_assigns (Qed)
+[wp] [Valid] typed_target5_extra_match_assigns (Qed)
+[wp] [Unsuccess] typed_target4_exact_match_ensures_post (Tactic) (Qed)
+[wp] [Unsuccess] typed_target5_extra_match_ensures_post (Tactic) (Qed)
+[wp] Proved goals: 9 / 12
+ Terminating: 3
+ Unreachable: 3
+ Qed: 3
+ Unsuccess: 3
+ Missing: 1
+------------------------------------------------------------
+ Function target3_no_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target3_no_match':
+Assume {
+ Type: is_sint32(x) /\ is_sint32(y) /\ is_sint32(z).
+ (* Pre-condition *)
+ Have: (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function target4_exact_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target4_exact_match':
+Assume {
+ Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(y) /\ is_sint32(z).
+ (* Pre-condition *)
+ Have: (r != 0) \/ (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/4:
+ - Post-condition 'post'
+ - Split (Case 1/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-0 (generated):
+Assume { Type: is_sint32(r). (* Case 1/4 *) When: r != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 2/4:
+ - Post-condition 'post'
+ - Split (Case 2/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-1 (generated):
+Assume { Type: is_sint32(x). (* Case 2/4 *) When: x != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 3/4:
+ - Post-condition 'post'
+ - Split (Case 3/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-2 (generated):
+Assume { Type: is_sint32(y). (* Case 3/4 *) When: y != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 4/4:
+ - Post-condition 'post'
+ - Split (Case 4/4)
+Goal Wp.Tactical.typed_target4_exact_match_ensures_post-3 (generated):
+Assume { Type: is_sint32(z). (* Case 4/4 *) When: z != 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function target5_extra_match
+------------------------------------------------------------
+
+Goal Post-condition 'post' in 'target5_extra_match':
+Assume {
+ Type: is_sint32(r) /\ is_sint32(s) /\ is_sint32(x) /\ is_sint32(y) /\
+ is_sint32(z).
+ (* Pre-condition *)
+ Have: (r != 0) \/ (s != 0) \/ (x != 0) \/ (y != 0) \/ (z != 0).
+}
+Prove: false.
+Prover Script returns Unsuccess
+
+------------------------------------------------------------
+Subgoal 1/5:
+ - Post-condition 'post'
+ - Split (Case 1/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-0 (generated):
+Assume { Type: is_sint32(r). (* Case 1/5 *) When: r != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 2/5:
+ - Post-condition 'post'
+ - Split (Case 2/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-1 (generated):
+Assume { Type: is_sint32(s). (* Case 2/5 *) When: s != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 3/5:
+ - Post-condition 'post'
+ - Split (Case 3/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-2 (generated):
+Assume { Type: is_sint32(x). (* Case 3/5 *) When: x != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 4/5:
+ - Post-condition 'post'
+ - Split (Case 4/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-3 (generated):
+Assume { Type: is_sint32(y). (* Case 4/5 *) When: y != 0. }
+Prove: false.
+
+------------------------------------------------------------
+Subgoal 5/5:
+ - Post-condition 'post'
+ - Split (Case 5/5)
+Goal Wp.Tactical.typed_target5_extra_match_ensures_post-4 (generated):
+Assume { Type: is_sint32(z). (* Case 5/5 *) When: z != 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ target3_no_match 1 - 2 50.0%
+ target4_exact_match 1 - 2 50.0%
+ target5_extra_match 1 - 2 50.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/pac.i b/src/plugins/wp/tests/wp_tip/pac.i
new file mode 100644
index 0000000000000000000000000000000000000000..78106ed2ac1214873dbe6f7c639c7c8336516c78
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/pac.i
@@ -0,0 +1,36 @@
+/* run.config
+ DONTRUN:
+*/
+
+/* run.config_qualif
+ OPT: -wp-status -wp-prover tip -wp-script dry
+ */
+
+/*@
+ strategy Split4:
+ \tactic("Wp.split"
+ ,\pattern( _ || _ || _ || _ )
+ );
+ proof Split4: post;
+*/
+
+/*@
+ requires x || y || z;
+ ensures post: \false;
+ assigns \nothing;
+*/
+void target3_no_match(int x, int y, int z) { return; }
+
+/*@
+ requires x || y || z || r;
+ ensures post: \false;
+ assigns \nothing;
+*/
+void target4_exact_match(int x, int y, int z, int r) { return; }
+
+/*@
+ requires x || y || z || r || s;
+ ensures post: \false;
+ assigns \nothing;
+*/
+void target5_extra_match(int x, int y, int z, int r, int s) { return; }