diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 8b168ade3d25030b702f8b61064ce06e2d266f67..8993d8dba42ee103cb5d87faa3660d22c4a33572 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -59,10 +59,29 @@ doing so would causing WP to add new cache entries to the global « qualif » ca
 from all your projects around. Consult the section « Global WP Cache Setup »
 below for details.
 
+# Qualified Test Results
+
+To be accepted by Frama-CI, tests in « qualif » configuration must be easily
+reproducible on any platform. This is checked by running WP with flag
+`-wp-msg-key success-only` which is set by the default in the qualif test
+configuration. Hence, a qualified test result only contains proof status that
+are either:
+- failed
+- valid for qed or script
+- cached for alt-ergo in all cases
+- valid, unknown or stepout for native Alt-Ergo
+- valid or unknown for (native) Coq
+
+This excludes any timeout with native Alt-Ergo, which must be turned into some
+reproducible stepout by setting `-wp-steps` and `-wp-timeout` options
+accordingly. Please choose a step limit that makes large enough to ensure the
+goal is not provable, but small enough to make alt-ergo decide quickly.
+
 # Global WP Cache Setup (for wp-qualif)
 
-All prover results for test configuration `qualif` shall be cached in a dedicate GitLab repo.
-This considerally speed-up the process of running those tests, from hours downto minutes.
+All prover results for test configuration `qualif` shall be cached in a dedicate
+GitLab repo.  This considerally speed-up the process of running those tests,
+from hours downto minutes.
 
 To ease the management of cache entries accross merge requests,
 _all_ cache entries shall be merged into the _same_ master branch of a global
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index 21e24fda36757762732f49c6098cceb82ab556bf..4384bb2f94134a59405d8a4370d6aff5ab66545e 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -332,7 +332,7 @@ Prove: foo_0 = 42.
 
 Goal Assertion 'bad' (file tests/wp/stmtcompiler_test.i, line 54):
 Prove: foo_0 = 42.
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 [wp] tests/wp/stmtcompiler_test.i:145: Warning: void object
@@ -352,7 +352,7 @@ Prove: foo_0 = 1.
 
 Goal Assertion 'bad' (file tests/wp/stmtcompiler_test.i, line 69):
 Prove: foo_0 = 1.
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 main_assigns_global sequent:
@@ -409,7 +409,7 @@ Prove: i = 1.
 Goal Assertion 'bad' (file tests/wp/stmtcompiler_test.i, line 87):
 Assume { Have: 0 <= x. }
 Prove: false.
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 zloop sequent:
@@ -592,7 +592,7 @@ Prove: x < 0.
 Goal Assertion 'bad' (file tests/wp/stmtcompiler_test.i, line 131):
 Assume { Have: 0 <= x. }
 Prove: false.
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 new way
@@ -621,7 +621,7 @@ Assume {
   Have: x_1 < (y * y).
 }
 Prove: false.
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 if_assert sequent:
@@ -656,7 +656,7 @@ Prove: x < (y * y).
 Goal Assertion (file tests/wp/stmtcompiler_test.i, line 140):
 Assume { Have: 0 <= x. }
 Prove: 0 < (x + (y * y)).
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 if_assert sequent:
@@ -670,7 +670,7 @@ Prove: x < (y * y).
 Goal Assertion (file tests/wp/stmtcompiler_test.i, line 137):
 Assume { Have: x < 0. }
 Prove: x < (y * y).
-[Qed] -
+[Qed] No Result
 
 ------------------------------------------------------------
 new way
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 26db574792afa1b3b397c090e23b6d9acb01bf53..f2c90674105083e0e3f44dddd5b6539770c92071 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -347,7 +347,7 @@ struct
            if result.verdict <> NoResult then
              Format.fprintf fmt "Prover %a returns %a@\n"
                pp_prover prover
-               pp_result result
+               (pp_result_qualif prover) result
         ) results ;
     end