diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 276f48908347b264601d7efebf40c3f907a84241..2ff1dcf688f516f2aa7f7c51c97382f71106b850 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -139,8 +139,8 @@ let select ~name ?version () =
     List.sort by_version @@ List.filter (filter ~name ?version) @@ provers ()
   with p::_ -> Some p | [] -> None
 
-let lookup ?(fallback=false) name =
-  match String.split_on_char ':' @@ String.lowercase_ascii name with
+let lookup ?(fallback=false) prover_name =
+  match String.split_on_char ':' @@ String.lowercase_ascii prover_name with
   | [name] -> select ~name ()
   | [name;version] ->
     begin
@@ -152,7 +152,8 @@ let lookup ?(fallback=false) name =
           | None -> None
           | Some p as res ->
             Wp_parameters.warning ~once:true
-              "Prover %s not found, fallback to %s" name (ident_wp p) ; res
+              "Prover %s not found, fallback to %s" prover_name (ident_wp p) ;
+            res
         else None
     end
   | _ -> None
diff --git a/src/plugins/wp/tests/wp_plugin/dune b/src/plugins/wp/tests/wp_plugin/dune
index 7323baff07fc5124c2e55b6e9e808096efbd1bdf..77a700def17a207f5ee1d2efb640bad964f9b4b8 100644
--- a/src/plugins/wp/tests/wp_plugin/dune
+++ b/src/plugins/wp/tests/wp_plugin/dune
@@ -2,6 +2,10 @@
  result_qualif/bitmask0x8000.0.session_qualif/script
  (copy_files ../../../bitmask0x8000.0.session_qualif/script/*))
 
+(subdir
+ result_qualif/fallback.0.session_qualif/script
+ (copy_files ../../../fallback.0.session_qualif/script/*))
+
 (subdir
  result_qualif/unroll.0.session_qualif/script
  (copy_files ../../../unroll.0.session_qualif/script/*))
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
new file mode 100644
index 0000000000000000000000000000000000000000..d180c4c3a1ebd2972ea065842cdc7dcfd4f52398
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/fallback.0.session_qualif/script/job_ensures.json
@@ -0,0 +1 @@
+[ { "prover": "Alt-Ergo:1.2.0", "verdict": "timeout", "time": 2. } ]
diff --git a/src/plugins/wp/tests/wp_plugin/fallback.i b/src/plugins/wp/tests/wp_plugin/fallback.i
index dc9e348288535b2cdfd414e8ca1d18001e598645..8cdadf45897a8cc614c4bf5f995283bd8d85ebf8 100644
--- a/src/plugins/wp/tests/wp_plugin/fallback.i
+++ b/src/plugins/wp/tests/wp_plugin/fallback.i
@@ -1,7 +1,9 @@
 /* run.config_qualif
-   EXIT: 1
-   OPT: -wp-prover=Alt-Ergo:1.2.0
+   DEPS: @PTEST_DEPS@ @WP_SESSION@/script/job_ensures.json
+   OPT: -wp-prover script @USING_WP_SESSION@
  */
 
-/*@ ensures \result == a * b ; */
-int job(int a,int b) { return (a - 1)*b + b ; }
+/*@ ensures \result <= 1000 ; */
+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 c31f09c80a4d0d475ee977e838297611a64b92b9..80aa41bf36e64609feef5679eb8e99dfb8d53838 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: (a * b) = x.
+Prove: x <= 1000.
 
 ------------------------------------------------------------
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 757ff0c0135f5d50e337f0d211bb91b603cb6583..6f5e911d7ab35354d90504505893dc715a1cb83b 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
@@ -4,11 +4,17 @@
 [wp] [Valid] Goal job_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal job_terminates (Cfg) (Trivial)
 [wp] Warning: Missing RTE guards
-[wp] User Error: Prover 'Alt-Ergo:1.2.0' not found in why3.conf
-[wp] Goal typed_job_ensures : not tried
+[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
+  Terminating:     1
+  Unreachable:     1
+  Unsuccess:       1
+  Missing:         1
+[wp] Session can be updated
+   - 1 script unused (now automated)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   job                       -        -        1       0.0%
 ------------------------------------------------------------
-[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Plug-in wp aborted: invalid user input.