diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 1a7bcaac2e5537c1df61a3f74dbecf06c3b16832..76ff4b3744348d4e0278ab2164424ae914c00bc6 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -162,7 +162,7 @@ let steps_seized steps steplimit =
   | None | Some 0 -> false
   | Some limit -> limit <= steps
 
-let promote ~timeout ~steplimit (res : VCS.result) =
+let promote ?timeout ?steplimit (res : VCS.result) =
   match res.verdict with
   | VCS.NoResult | VCS.Computing _ -> VCS.no_result
   | VCS.Failed -> res
@@ -273,7 +273,7 @@ let get_result ~digest ~runner ~timeout ~steplimit prover goal =
     let hash = lazy (digest prover goal) in
     let result =
       get_cache_result ~mode hash
-      |> promote ~timeout ~steplimit |> VCS.cached in
+      |> promote ?timeout ?steplimit |> VCS.cached in
     if VCS.is_verdict result
     then
       begin
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index f017a12efebc467e71fd04eb4d5a678dbedf045d..5ee0e5deec01408f4c1c2c5e1d9f00b1f33576e3 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -41,6 +41,11 @@ type 'a runner =
   timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a ->
   VCS.result Task.task
 
+val promote: ?timeout:float -> ?steplimit:int -> VCS.result -> VCS.result
+(** Converts some known results to the given limits.
+    In particular, if the result shall be discarded with respect to the limits,
+    the function returns [VCS.no_result]. *)
+
 val get_result: digest:('a digest) -> runner:('a runner) -> 'a runner
 val clear_result: digest:('a digest) -> Why3Provers.t -> 'a -> unit
 
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 9277e1d3beb3223b9d06074ea1f506ab5b3f7e0f..bb8daa671f0645d85cf2c71bc14e4fe343a3db62 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -349,7 +349,7 @@ and explore_provers env alternative : solver =
 
 and explore_prover env timeout prover node =
   let wpo = ProofEngine.goal node in
-  let result = Wpo.get_result wpo prover in
+  let result = Cache.promote ~timeout @@ Wpo.get_result wpo prover in
   if VCS.is_valid result then success else
   if VCS.is_verdict result then failed else
     let config = { VCS.default with timeout = Some timeout } in