diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 2ff1dcf688f516f2aa7f7c51c97382f71106b850..204a593d6d3948bc2dcc7e24d08df3c5194f0bd4 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -151,7 +151,7 @@ let lookup ?(fallback=false) prover_name =
           match select ~name () with
           | None -> None
           | Some p as res ->
-            Wp_parameters.warning ~once:true
+            Wp_parameters.warning ~once:true ~current:false
               "Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
             res
         else None
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
index d180c4c3a1ebd2972ea065842cdc7dcfd4f52398..2f92c64659efb2b81d45b139a3336994508cb838 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
+++ b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
@@ -1 +1 @@
-[ { "prover": "Alt-Ergo:1.2.0", "verdict": "timeout", "time": 2. } ]
+[ { "prover": "Alt-Ergo:1.2.0", "verdict": "valid", "time": 0.1 } ]
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index 8cdadf45897a8cc614c4bf5f995283bd8d85ebf8..b4ec19b80dfbeaff50d1d8ffd6fa17db2d7dfe8e 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,9 +1,9 @@
 /* run.config_qualif
    DEPS: @PTEST_DEPS@ @WP_SESSION@/script/job_ensures.json
-   OPT: -wp-prover script @USING_WP_SESSION@
+   OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@
  */
 
-/*@ ensures \result <= 1000 ; */
+/*@ ensures \result == a * b ; */
 int job(int a,int b){
   return (a - 1) * b + b ;
 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
index 80aa41bf36e64609feef5679eb8e99dfb8d53838..c31f09c80a4d0d475ee977e838297611a64b92b9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/fallback.res.oracle
@@ -11,6 +11,6 @@
 Goal Post-condition (file fallback.i, line 6) in 'job':
 Let x = b + (b * (a - 1)).
 Assume { Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(x). }
-Prove: x <= 1000.
+Prove: (a * b) = x.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index 6f5e911d7ab35354d90504505893dc715a1cb83b..6c923007a1824b9a86158c4527d8a020be54e708 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -5,16 +5,15 @@
 [wp] [Valid] Goal job_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
-[wp] :0: Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
-[wp] [NoResult] typed_job_ensures (Qed)
-[wp] Proved goals:    2 / 3
+[wp] Warning: Prover Alt-Ergo:1.2.0 not found, fallback to Alt-Ergo:2.5.3
+[wp] [Valid] typed_job_ensures (Alt-Ergo) (Cached)
+[wp] Proved goals:    3 / 3
   Terminating:     1
   Unreachable:     1
-  Unsuccess:       1
-  Missing:         1
+  Alt-Ergo:        1
 [wp] Session can be updated
    - 1 script unused (now automated)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  job                       -        -        1       0.0%
+  job                       -        1        1       100%
 ------------------------------------------------------------