diff --git a/src/plugins/wp/tests/wp_plugin/cfg.c b/src/plugins/wp/tests/wp_plugin/cfg.c
index 0c0a510591c31a3e1074d13742043bd4614be76a..76b6505c4cf0e176c6e0bd8f35488faaf06db478 100644
--- a/src/plugins/wp/tests/wp_plugin/cfg.c
+++ b/src/plugins/wp/tests/wp_plugin/cfg.c
@@ -1,7 +1,7 @@
//@ assigns \nothing;
void foo(void);
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1(void)
{
if (0 == 1)
@@ -14,7 +14,7 @@ void f1(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1_simpler(void)
{
if (0 == 1)
@@ -26,7 +26,7 @@ void f1_simpler(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1_variant(void)
{
if (0 == 1) L: ;
@@ -50,7 +50,7 @@ void f1_variant_invert(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f2(void)
{
if (0 == 1)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
index f78e97da034cdcae042c07a28d2fdb21a6fead50..7f60486d328f49305869a1dfd91400fa33f89340 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
@@ -6,24 +6,24 @@
Function f1
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function f1_simpler
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1_simpler':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1_simpler':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function f1_variant
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1_variant':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1_variant':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
@@ -38,7 +38,7 @@ Prove: false.
Function f2
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f2':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f2':
+Prove: false.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
index 65a2d69e16bdb23fa6a41746dccb152924467752..9fc9c79a7806a7a9fac3c119348f7adafa40e0b6 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
@@ -3,19 +3,18 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Qed] Goal typed_f1_ensures_BUG_WP : Valid
-[wp] [Qed] Goal typed_f1_simpler_ensures_BUG_WP : Valid
-[wp] [Qed] Goal typed_f1_variant_ensures_BUG_WP : Valid
+[wp] [Alt-Ergo] Goal typed_f1_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f1_simpler_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f1_variant_ensures_BUG_LEGACY_WP : Unsuccess
[wp] [Alt-Ergo] Goal typed_f1_variant_invert_ensures_FAILS_AS_EXPECTED : Unsuccess
-[wp] [Qed] Goal typed_f2_ensures_BUG_WP : Valid
-[wp] Proved goals: 4 / 5
- Qed: 4
- Alt-Ergo: 0 (unsuccess: 1)
+[wp] [Alt-Ergo] Goal typed_f2_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] Proved goals: 0 / 5
+ Alt-Ergo: 0 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f1 1 - 1 100%
- f1_simpler 1 - 1 100%
- f1_variant 1 - 1 100%
+ f1 - - 1 0.0%
+ f1_simpler - - 1 0.0%
+ f1_variant - - 1 0.0%
f1_variant_invert - - 1 0.0%
- f2 1 - 1 100%
+ f2 - - 1 0.0%
------------------------------------------------------------