diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index c9693efd719de9374a866e8dbe6f619b095f781e..6444533328f30bf4535ff92e0bc6b826793bc71d 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -665,9 +665,10 @@ class pane (gprovers : GuiConfig.provers) =
                 self#search proof fork
               else
                 begin
+                  let provers = List.map (fun e -> e#prover) provers in
                   ProverScript.search
                     ~depth ~width ~auto
-                    ~provers:[ VCS.NativeAltErgo ]
+                    ~provers
                     ~result:
                       (fun wpo prv res ->
                          text#printf "[%a] %a : %a@."
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 1e9a0feae7cd9372939cd1f55a56a0d8c1b37d57..0dc36e0245fa1c3d68e1f6a67d60f62926efae6a 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -404,9 +404,14 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
                 ~steps verdict
             with Not_found ->
               begin
+                let message std =
+                  Format.asprintf
+                    "Alt-Ergo (%s) for goal %a"
+                    std WpPropId.pretty pid
+                in
                 if Wp_parameters.verbose_atleast 1 then begin
-                  ProverTask.pp_file ~message:"Alt-Ergo (stdout)" ~file:logout ;
-                  ProverTask.pp_file ~message:"Alt-Ergo (stderr)" ~file:logerr ;
+                  ProverTask.pp_file ~message:(message "stdout") ~file:logout ;
+                  ProverTask.pp_file ~message:(message "stderr") ~file:logerr ;
                 end;
                 if r = 0 then VCS.failed "Unexpected Alt-Ergo output"
                 else VCS.kfailed "Alt-Ergo exits with status [%d]." r
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 7a264f1e5f55a90b2df5bc1924e92f40d928a839..50d397972326abe6dc05b733e556640ccd851863 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -324,7 +324,8 @@ let rec crawl env on_child node = function
       Task.return ()
 
   | Error(msg,json) :: alternative ->
-      Wp_parameters.warning "@[<hov 2>Script Error %S: %a@]@."
+      Wp_parameters.warning "@[<hov 2>Script Error: on goal %a@\n%S: %a@]@."
+        WpPropId.pretty (Env.goal env node).po_pid
         msg Json.pp json ;
       crawl env on_child node alternative
 
@@ -349,9 +350,11 @@ let rec crawl env on_child node = function
         match jfork (Env.tree env) ?node jtactic with
         | None ->
             Wp_parameters.warning
-              "Script Error: can not apply '%s'@\n\
+              "Script Error: on goal %a@\n\
+               can not apply '%s'@\n\
                @[<hov 2>Params: %a@]@\n\
                @[<hov 2>Select: %a@]@."
+              WpPropId.pretty (Env.goal env node).po_pid
               jtactic.tactic
               Json.pp jtactic.params
               Json.pp jtactic.select ;