diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index e9b4d301ca5d6aedeaab1a7ddf538d2abe759404..2a96d02786da0b24a96f48fc92f717f41171cb8e 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -392,16 +392,19 @@ let task
     ~depth ~width ~backtrack ~auto
     ~start ~progress ~result ~success wpo =
   begin fun () ->
-    start wpo ;
-    let json = ProofSession.load wpo in
-    let script = Priority.sort (ProofScript.decode json) in
-    let tree = ProofEngine.proof ~main:wpo in
-    let env = Env.make tree
-        ~valid ~failed ~provers
-        ~depth ~width ~backtrack ~auto
-        ~progress ~result ~success in
-    crawl env (process env) None script >>?
-    (fun _ -> ProofEngine.forward tree) ;
+    Prover.simplify ~start ~result wpo >>= fun succeed ->
+    if succeed
+    then Task.return ()
+    else
+      let json = ProofSession.load wpo in
+      let script = Priority.sort (ProofScript.decode json) in
+      let tree = ProofEngine.proof ~main:wpo in
+      let env = Env.make tree
+          ~valid ~failed ~provers
+          ~depth ~width ~backtrack ~auto
+          ~progress ~result ~success in
+      crawl env (process env) None script >>?
+      (fun _ -> ProofEngine.forward tree) ;
   end
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/prover.mli b/src/plugins/wp/prover.mli
index 6a2711c2704f71a1ba7ba1f2e7346f3728aa83f1..32e1ca6ff6a93ba513a1851a0f108fb008ba5df1 100644
--- a/src/plugins/wp/prover.mli
+++ b/src/plugins/wp/prover.mli
@@ -26,6 +26,11 @@ open VCS
 (* --- Prover Implementation against Task API                             --- *)
 (* -------------------------------------------------------------------------- *)
 
+val simplify :
+  ?start:(Wpo.t -> unit) ->
+  ?result:(Wpo.t -> prover -> result -> unit) ->
+  Wpo.t -> bool Task.task
+
 val prove : Wpo.t ->
   ?config:config ->
   ?mode:mode ->
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index e84e2fec240b3cab00f04650aed8a9fef553f53d..867d238326d1fedb1c8bc7903b992f091fd18874 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -814,8 +814,7 @@ let resolve g =
   let valid = reduce g in
   if valid then
     let result = VCS.result ~solver:(qed_time g) VCS.Valid in
-    ignore (set_result g VCS.Qed result) ;
-    true
+    ( set_result g VCS.Qed result ; true )
   else false
 
 let compute g =