[wp] replay stronger prover alternative

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

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
 

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