diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 94248faed18a00b9d3e6ef53a09588f184621420..1a3e5223da2e0b38362bb7a99481de429be9dad6 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
 #   <Prover>: prover
 ###############################################################################
 
+- WP          [2019/12/04] Added option -wp-run-all-provers
+
 ##########################
 Plugin WP 20.0 (Calcium)
 ##########################
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index a2e6ea942697d83376ea55d968f1922ede00a6b9..4018a3accb411c4214fbf75804eaddf4549044a2 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -320,7 +320,7 @@ let spawn ?(monitor=silent) ?pool (jobs : ('a * bool Task.task) list) =
       let canceled = ref false in
       let callback a r =
         if r then
-          begin if not !canceled then
+          begin if not !canceled && not (Wp_parameters.RunAllProvers.get()) then
               begin
                 canceled := true ;
                 monitor (Some a) ;
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 3d0330f4f5b5917ddd50e6ab4c77cfed1bbfa1a3..82d7691f3e1c8e13d0054e1314937c891a7ea2af 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -995,6 +995,9 @@ Support for \textsf{Why-3 IDE} is no longer provided.
   installing \textsf{Frama-C}.
   The option reads your \textsf{Why-3} configuration and prints the available
   provers with their \verb+-wp-prover <p>+ code names.
+\item[\tt -wp-(no)-run-all-provers] Run all specified provers on each goal not
+  proved by Qed. When a prover succeeds in proving the goal, the others are not
+  stopped. (default is: no).
 \item[\tt -wp-gen] only generates proof obligations, does not run provers.
   See option \texttt{-wp-out} to obtain the generated proof obligations.
 \item[\tt -wp-par <n>] limits the number of parallel process runs for
@@ -1241,7 +1244,7 @@ interactively or incrementally, it is often the case where most proof obligation
 from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
 and stored in your session.
 
-% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers. 
+% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers.
 There are different ways of using the cache, depending on your precise needs.
 The main option to control cache usage is \verb+-wp-cache+, documented below:
 
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 54249649895013f4b56a7bf7cc421d5129875e68..9405a7c288825677007d155f0c41ee6143105ec9 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -567,6 +567,14 @@ module Provers = String_list
         "
     end)
 
+let () = Parameter_customize.set_group wp_prover
+module RunAllProvers =
+  False(struct
+    let option_name = "-wp-run-all-provers"
+    let help = "Run all specified provers on each goal not proved by Qed. \
+                Do not stop when a prover succeeds. (default: no)"
+  end)
+
 let () = Parameter_customize.set_group wp_prover
 module Cache = String
     (struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 3429afff23bf26b541eeea063d58f526cfc04854..38cfee00fed7044ebfc6b029e41d527c9d5bbe0d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -105,6 +105,7 @@ module PrecondWeakening : Parameter_sig.Bool
 module Detect: Parameter_sig.Bool
 module Generate:Parameter_sig.Bool
 module Provers: Parameter_sig.String_list
+module RunAllProvers: Parameter_sig.Bool
 module Cache: Parameter_sig.String
 module Drivers: Parameter_sig.String_list
 module Script: Parameter_sig.String