diff --git a/Makefile b/Makefile
index add6a8e330e945f5b3de056c421b576856484cb4..fa0c654f9a9b6504f4bde849902c2948c72f9a82 100644
--- a/Makefile
+++ b/Makefile
@@ -945,7 +945,7 @@ PLUGIN_NAME:=Reduc
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/reduc
PLUGIN_CMO:=reduc_options misc value2acsl collect hyp register
-PLUGIN_DEPENDENCIES:=Value
+PLUGIN_DEPENDENCIES:=Eva
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0aceb023406b9948286a3ac5b744377ddf766def
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
@@ -0,0 +1,26 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva1' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:34: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Alt-Ergo] Goal eva1_f_assert : Failed
+ [Why3 Error] Not a predicate symbol: write_sint32
+[wp] [Alt-Ergo] Goal eva1_f_assert_Eva_division_by_zero : Failed
+ [Why3 Error] Not a predicate symbol: write_sint321
+[wp] Failure: Undefined symbol 'read_sint32'
+[wp] [Alt-Ergo] Goal eva1_g_assert : Failed
+ [Why3 Error] anomaly: Log.AbortFatal("wp")
+[wp] Proved goals: 0 / 3
+ Alt-Ergo: 0 (failed: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - - 2 0.0%
+ g - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..21d94a667b9c9477d12b9b06df0a302941fb0a60
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva2' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:34: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Alt-Ergo] Goal eva2_f_assert : Timeout (missing cache)
+[wp] [Alt-Ergo] Goal eva2_f_assert_Eva_division_by_zero : Valid (missing cache)
+[wp] [Alt-Ergo] Goal eva2_g_assert : Timeout (missing cache)
+[wp] Proved goals: 1 / 3
+ Qed: 0
+ Alt-Ergo: 1 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - 1 2 50.0%
+ g - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/simple.c b/src/plugins/wp/tests/wp_eva/simple.c
index 4e5a58321e7c70d96becf638c5f5992922a0f884..728d2b49d2a2af56f32f896bd8677236f3e8119c 100644
--- a/src/plugins/wp/tests/wp_eva/simple.c
+++ b/src/plugins/wp/tests/wp_eva/simple.c
@@ -1,3 +1,13 @@
+/* run.config
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
+/* run.config_qualif
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
#include "__fc_builtin.h"
/*@
@@ -10,8 +20,10 @@
int z;
void f (int *x, int *y){
+ if(z==41) return;
*x = *x+1;
/*@ assert P(*x) && P(*y) && P(z); @*/
+ int r = 1/(*x-42);
}
void g (int *x, int *y){
diff --git a/src/plugins/wp/tests/wp_eva/test_config b/src/plugins/wp/tests/wp_eva/test_config
index c01e5325329837427b6260c71f109832da34cf7a..8b6102546cc5b9169aa4d10d195b2ef2f5bab0b3 100644
--- a/src/plugins/wp/tests/wp_eva/test_config
+++ b/src/plugins/wp/tests/wp_eva/test_config
@@ -1,3 +1 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope -eva -load-module wp -eva-no-print -eva-verbose 0
-OPT: -then -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell -wp-model eva1
-OPT: -then -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell -wp-model eva2
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell
diff --git a/src/plugins/wp/tests/wp_eva/test_config_qualif b/src/plugins/wp/tests/wp_eva/test_config_qualif
new file mode 100644
index 0000000000000000000000000000000000000000..153e5ddde393c7008e0ff327852ba9b948a25e54
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -0,0 +1,2 @@
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+OPT: