diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
new file mode 100644
index 0000000000000000000000000000000000000000..1a1174504f7e46923c594d5f5d11049ad5fdd1f0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -0,0 +1,19 @@
+/* run.config
+   OPT: -eva -load-module scope,eva,report -then -report
+   OPT: -wp-prop=@check
+   OPT: -wp-prop=@assert
+*/
+/* run.config_qualif
+   OPT: -load-module report -wp-steps 5 -then -report
+*/
+
+// note: eva and wp gives the same reporting
+
+//@ axiomatic A { predicate P reads \nothing ; }
+void main() {
+  //@check  c1: P;
+  //@assert a1: P;
+  //@check  c2: P;
+  //@assert a2: P;
+  ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a99ec33e26d36787a9fc88e173e145acb5ac2b4a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -0,0 +1,75 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva:alarm] tests/wp_acsl/checks.i:14: Warning: check 'c1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:15: Warning: 
+  assertion 'a1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:16: Warning: check 'c2' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:17: Warning: 
+  assertion 'a2' got status unknown.
+[eva] done for function main
+[scope:rm_asserts] removing 2 assertion(s)
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[  Valid  ] Axiomatic 'A'
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[    -    ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+            tried with Eva.
+[    -    ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+            tried with Eva.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+            By RedundantAlarms, with pending:
+             - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+            By RedundantAlarms, with pending:
+             - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+     1 Completely validated
+     2 Locally validated
+     2 To be validated
+     5 Total
+--------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6de4c09508772db4e0a498cd8342d9401c6e88eb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..669139a5ea8ea941f92baa78c54e794707a355ec
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7f27fd0f13f0ebe09ac0befc560084d9b6d8beb5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 5 [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_main_check_c1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_assert_a1 : Unsuccess
+[wp] [Qed] Goal typed_main_check_c2 : Valid
+[wp] [Qed] Goal typed_main_assert_a2 : Valid
+[wp] Proved goals:    2 / 4
+  Qed:             2 
+  Alt-Ergo:        0  (unsuccess: 2)
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/checks.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/checks.0.report.json'
+-------------------------------------------------------------
+Functions           WP     Alt-Ergo        Total   Success
+main                 2     -                 4      50.0%
+-------------------------------------------------------------
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[  Valid  ] Axiomatic 'A'
+            by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[    -    ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+            tried with Wp.typed.
+[    -    ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+            tried with Wp.typed.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+            By Wp.typed, with pending:
+             - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+            By Wp.typed, with pending:
+             - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+     1 Completely validated
+     2 Locally validated
+     2 To be validated
+     5 Total
+--------------------------------------------------------------------------------