diff --git a/src/plugins/wp/tests/wp_plugin/doomed_pre.i b/src/plugins/wp/tests/wp_plugin/doomed_pre.i
index 104c9ec932ce1263aa3fcc90b0037574ddf43dfa..d7be0aa8c9a95835f78b720590d4f5a971a397a0 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_pre.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_pre.i
@@ -7,13 +7,34 @@
*/
//@ requires a < 0 && a > 0 ;
-void default_requires(int a){}
+void requires(int a){}
/*@ requires a < 0 ;
behavior B:
assumes a > 0 ;
*/
-void default_reqs_assumes(int a){}
+void reqs_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B:
+ assumes a > 0 ;
+ assumes a > 1 ;
+*/
+void reqs_2_2_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B:
+ assumes a > 0 ;
+ assumes a < -42 ;
+*/
+void reqs_1_2_assumes(int a){}
+
+/*@ requires a >= 0 ;
+ behavior B:
+ assumes a > 10 ;
+ assumes a < 10 ;
+*/
+void reqs_combined_assumes(int a){}
/*@ behavior B:
assumes a < 0 && a > 0 ; // not detected
@@ -25,3 +46,11 @@ void only_assumes(int a){}
requires a < 0 ;
*/
void bhv_requires_assumes(int a){}
+
+/*@ requires a < 0 ;
+ behavior B1:
+ assumes a > 0 ;
+ behavior B2:
+ assumes a > 1 ;
+*/
+void reqs_massumes(int a){}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
index b472440a78e10466522fec758cbf776da599c3f5..fe70e5a3f43446af7c7f6dd0390d6eeccff8d88d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_pre.res.oracle
@@ -11,27 +11,103 @@ Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function default_reqs_assumes
+ Function reqs_1_2_assumes
------------------------------------------------------------
-Goal Wp_smoke_default_requires in 'default_reqs_assumes':
+Goal Wp_smoke_default_requires in 'reqs_1_2_assumes':
Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
- Function default_reqs_assumes with behavior B
+ Function reqs_1_2_assumes with behavior B
------------------------------------------------------------
-Goal Wp_smoke_B_assumes in 'default_reqs_assumes':
+Goal Wp_smoke_B_assumes in 'reqs_1_2_assumes':
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
- Function default_requires
+ Function reqs_2_2_assumes
------------------------------------------------------------
-Goal Wp_smoke_default_requires in 'default_requires':
+Goal Wp_smoke_default_requires in 'reqs_2_2_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_2_2_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_2_2_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_combined_assumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_combined_assumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: 0 <= a. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_combined_assumes with behavior B
+------------------------------------------------------------
+
+Goal Wp_smoke_B_assumes in 'reqs_combined_assumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'reqs_massumes':
+Assume { Type: is_sint32(a). (* Pre-condition *) Have: a < 0. }
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes with behavior B1
+------------------------------------------------------------
+
+Goal Wp_smoke_B1_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function reqs_massumes with behavior B2
+------------------------------------------------------------
+
+Goal Wp_smoke_B2_assumes in 'reqs_massumes':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function requires
+------------------------------------------------------------
+
+Goal Wp_smoke_default_requires in 'requires':
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
index 80e10bd4d498b31b25b7ec1391ba9be8de6a5709..34eb51d822f54facf0cfd3de01835067da2b6867 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
@@ -2,23 +2,46 @@
[kernel] Parsing tests/wp_plugin/doomed_pre.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 4 goals scheduled
-[wp] [Failed] Smoke-test typed_default_requires_wp_smoke_default_requires
+[wp] 13 goals scheduled
+[wp] [Failed] Smoke-test typed_requires_wp_smoke_default_requires
Qed: Valid
[wp] tests/wp_plugin/doomed_pre.i:10: Warning: Failed smoke-test
-[wp] [Passed] Smoke-test typed_default_reqs_assumes_wp_smoke_default_requires
-[wp] [Failed] Smoke-test typed_default_reqs_assumes_wp_smoke_B_assumes
+[wp] [Passed] Smoke-test typed_reqs_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_assumes_wp_smoke_B_assumes
Qed: Valid
[wp] tests/wp_plugin/doomed_pre.i:16: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_2_2_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:23: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_1_2_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:30: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_combined_assumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_combined_assumes_wp_smoke_B_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:37: Warning: Failed smoke-test
[wp] [Failed] Smoke-test typed_bhv_requires_assumes_wp_smoke_B_requires
Qed: Valid
-[wp] tests/wp_plugin/doomed_pre.i:27: Warning: Failed smoke-test
-[wp] Proved goals: 1 / 4
- Qed: 0 (failed: 3)
- Alt-Ergo: 1
+[wp] tests/wp_plugin/doomed_pre.i:48: Warning: Failed smoke-test
+[wp] [Passed] Smoke-test typed_reqs_massumes_wp_smoke_default_requires
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B1_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed] Smoke-test typed_reqs_massumes_wp_smoke_B2_assumes
+ Qed: Valid
+[wp] tests/wp_plugin/doomed_pre.i:56: Warning: Failed smoke-test
+[wp] Proved goals: 5 / 13
+ Qed: 0 (failed: 8)
+ Alt-Ergo: 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- default_requires - - 1 0.0%
- default_reqs_assumes - 1 2 50.0%
+ requires - - 1 0.0%
+ reqs_assumes - 1 2 50.0%
+ reqs_2_2_assumes - 1 2 50.0%
+ reqs_1_2_assumes - 1 2 50.0%
+ reqs_combined_assumes - 1 2 50.0%
bhv_requires_assumes - - 1 0.0%
+ reqs_massumes - 1 3 33.3%
------------------------------------------------------------