diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index f7a23b616734d7626041a80d8a28854b83e85391..a6d0ebcd8f60c9bcfcc64c8b3773f15bc20790ea 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -36,7 +36,7 @@ let error = function
 (* ------------------------------------------------------------------------ *)
 
 type 'a status =
-  | Timeout of int
+  | Timeout of float
   | Canceled
   | Result of 'a
   | Failed of exn
@@ -206,7 +206,7 @@ let sync m t = lock m >>= t >>? fun _ -> unlock m
 type cmd = {
   name : string ;
   timed : bool ;
-  timeout : int ;
+  timeout : float ;
   time_start : float ;
   time_stop : float ;
   mutable time_killed : bool ;
@@ -227,9 +227,9 @@ let start_command ~timeout ?time ?stdout ?stderr cmd args =
          Format.pp_print_string fmt cmd ;
          Array.iter
            (fun c -> Format.fprintf fmt "@ %s" c) args) ;
-    let timed = timeout > 0 || time <> None in
+    let timed = timeout > 0.0 || time <> None in
     let time_start = if timed then Unix.gettimeofday () else 0.0 in
-    let time_stop = if timeout > 0 then time_start +. float_of_int timeout else 0.0 in
+    let time_stop = if timeout > 0.0 then time_start +. timeout else 0.0 in
     let async = Command.command_async ?stdout ?stderr cmd args in
     {
       name = cmd ;
@@ -251,7 +251,7 @@ let ping_command cmd coin =
       if coin = Kill then (kill () ; Wait 100)
       else
         let time_now = if cmd.timed then Unix.gettimeofday () else 0.0 in
-        if cmd.timeout > 0 && time_now > cmd.time_stop then
+        if cmd.timeout > 0.0 && time_now > cmd.time_stop then
           begin
             set_time cmd (time_now -. cmd.time_start) ;
             Kernel.debug ~dkey:Kernel.dkey_task "timeout '%s'" cmd.name ;
@@ -282,7 +282,7 @@ let ping_command cmd coin =
       "failure '%s' [%s]" cmd.name (Printexc.to_string e) ;
     Return (Failed e)
 
-let command ?(timeout=0) ?time ?stdout ?stderr cmd args = todo
+let command ?(timeout=0.0) ?time ?stdout ?stderr cmd args = todo
     begin fun () ->
       let cmd = start_command ~timeout ?time ?stdout ?stderr cmd args in
       Monad.async (ping_command cmd)
diff --git a/src/libraries/utils/task.mli b/src/libraries/utils/task.mli
index 02de39e228b85e6fe645975d6211acd643b2d9d2..fb33ce9f7086a980d09a6bd700c2b9789679b976 100644
--- a/src/libraries/utils/task.mli
+++ b/src/libraries/utils/task.mli
@@ -29,7 +29,7 @@
 
 type 'a task
 type 'a status =
-  | Timeout of int
+  | Timeout of float
   | Canceled
   | Result of 'a
   | Failed of exn
@@ -134,7 +134,7 @@ val sync : mutex -> (unit -> 'a task) -> 'a task
 (* ************************************************************************* *)
 
 val command :
-  ?timeout:int ->
+  ?timeout:float ->
   ?time:float ref ->
   ?stdout:Buffer.t ->
   ?stderr:Buffer.t ->
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 6a60e4b06802e14ad3e7e258c436199f8208e917..1a7bcaac2e5537c1df61a3f74dbecf06c3b16832 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -145,16 +145,16 @@ let is_updating = function
   | Update | Rebuild | Cleanup -> true
 
 let time_fits time = function
-  | None | Some 0 -> true
-  | Some limit -> time <= float limit
+  | None | Some 0.0 -> true
+  | Some limit -> time <= limit
 
 let steps_fits steps = function
   | None | Some 0 -> true
   | Some limit -> steps <= limit
 
 let time_seized time = function
-  | None | Some 0 -> false
-  | Some limit -> float limit <= time
+  | None | Some 0.0 -> false
+  | Some limit -> limit <= time
 
 let steps_seized steps steplimit =
   steps <> 0 &&
@@ -257,7 +257,7 @@ type 'a digest =
   Why3Provers.t -> 'a -> string
 
 type 'a runner =
-  timeout:int option -> steplimit:int option -> Why3Provers.t -> 'a ->
+  timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a ->
   VCS.result Task.task
 
 let get_result ~digest ~runner ~timeout ~steplimit prover goal =
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index 928acecfa3d21d93fc63aec1ef9687d41b2dcae6..f017a12efebc467e71fd04eb4d5a678dbedf045d 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -38,7 +38,7 @@ val cleanup_cache : unit -> unit
 type 'a digest = Why3Provers.t -> 'a -> string
 
 type 'a runner =
-  timeout:int option -> steplimit:int option -> Why3Provers.t -> 'a ->
+  timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a ->
   VCS.result Task.task
 
 val get_result: digest:('a digest) -> runner:('a runner) -> 'a runner
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 72838dc8ee20d39adcf5b6d4a96de5383db7c783..841808a4dbf6912aed982070cfe321c466faac30 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
 Plugin WP <next-release>
 ###############################################################################
 
+- WP          [2023-04-03] Default timeout set to 2s
 - WP          [2023-03-29] fix option -wp-split to only split conditions
 - WP          [2023-03-29] new option -wp-split-switch to split switches
 - WP          [2023-03-29] new option -wp-split-conj to split conjunctive goals
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index 4746c8b00f0551b1b858876e32079de5c4e53f4f..76808660184319c903f6b9d4c49e64fdbaf88ad7 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -182,7 +182,7 @@ class command name =
     val mutable once = true
     val mutable cmd = name
     val mutable param : string list = []
-    val mutable timeout = 0
+    val mutable timeout = 0.0
     val mutable validout = []
     val mutable validerr = []
     val mutable timers = []
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index db6356dbe219ca14fbbf6551cd2fce6f81bb9ff1..a37c089fdbefc34b97ab1064128a91edfa59473d 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -77,7 +77,7 @@ class virtual command : string ->
     method add_float : name:string -> value:float -> unit
     method add_parameter : name:string -> (unit -> bool) -> unit
     method add_list : name:string -> string list -> unit
-    method timeout : int -> unit
+    method timeout : float -> unit
     method validate_time : (float -> unit) -> unit
     method validate_pattern : ?logs:logs -> ?repeat:bool ->
       Str.regexp -> (pattern -> unit) -> unit
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 834e02cd47ed7a8e2c306e6782c4261e66fe1199..c2845393a30da832cc0cbf934ca5ab4e514ef030 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1152,7 +1152,7 @@ type prover_call = {
   prover : Why3Provers.t ;
   call : Why3.Call_provers.prover_call ;
   steps : int option ;
-  timeout : int ;
+  timeout : float ;
   mutable timeover : float option ;
   mutable interrupted : bool ;
   mutable killed : bool ;
@@ -1163,11 +1163,11 @@ let ping_prover_call ~config p =
   | NoUpdates
   | ProverStarted ->
     let () =
-      if p.timeout > 0 then
+      if p.timeout > 0.0 then
         match p.timeover with
         | None ->
           let started = Unix.time () in
-          p.timeover <- Some (started +. 2.0 +. float p.timeout)
+          p.timeover <- Some (started +. 2.0 +. p.timeout)
         | Some timeout ->
           let time = Unix.time () in
           if time > timeout then
@@ -1187,7 +1187,7 @@ let ping_prover_call ~config p =
   | ProverFinished pr ->
     let r =
       match pr.pr_answer with
-      | Timeout -> VCS.timeout (int_of_float pr.pr_time)
+      | Timeout -> VCS.timeout pr.pr_time
       | Valid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Valid
       | Invalid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Invalid
       | OutOfMemory -> VCS.failed "out of memory"
@@ -1211,11 +1211,11 @@ let ping_prover_call ~config p =
     Task.Return (Task.Result r)
 
 let call_prover_task ~timeout ~steps ~config prover call =
-  Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %d, steps %d@."
+  Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %f, steps %d@."
     Why3.Whyconf.print_prover prover
-    (Why3.Opt.get_def (-1) timeout)
-    (Why3.Opt.get_def (-1) steps) ;
-  let timeout = match timeout with None -> 0 | Some tlimit -> tlimit in
+    (Why3.Opt.get_def (0.0) timeout)
+    (Why3.Opt.get_def 0 steps) ;
+  let timeout = match timeout with None -> 0.0 | Some tlimit -> tlimit in
   let pcall = {
     call ; prover ;
     killed = false ;
@@ -1256,7 +1256,6 @@ let run_batch pconf driver ~config ?script ~timeout ~steplimit prover task =
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
   let limit =
     let config = Why3.Whyconf.get_main @@ Why3Provers.config () in
-    let timeout = Option.map float_of_int timeout in
     let memlimit = Why3.Whyconf.memlimit config in
     let def = Why3.Call_provers.empty_limit in
     { Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
@@ -1343,7 +1342,7 @@ let prepare ~mode wpo driver task =
 
 let interactive ~mode wpo pconf ~config driver prover task =
   let time = Wp_parameters.InteractiveTimeout.get () in
-  let timeout = if time <= 0 then None else Some time in
+  let timeout = if time <= 0 then None else Some (float time) in
   match prepare ~mode wpo driver task with
   | None ->
     Wp_parameters.warning ~once:true ~current:false
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 8f00f859dfa4a8b5200980a0ff053b2476e24efb..24aac04061dc75bf6f294910899857c8f49e2e4f 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -26,7 +26,7 @@ val add_specific_equality:
   unit
 (** Equality used in the goal, simpler to prove than polymorphic equality *)
 
-val prove : ?mode:VCS.mode -> ?timeout:int -> ?steplimit:int ->
+val prove : ?mode:VCS.mode -> ?timeout:float -> ?steplimit:int ->
   prover:Why3Provers.t -> Wpo.t -> VCS.result Task.task
 (** Return NoResult if it is already proved by Qed *)
 
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 60caa14eb5be10d93b07163d2f61dd2d31b3a182..50449ec8a3b466e59467fa38fc3610b3f368ae4f 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -86,9 +86,10 @@ let ptime t valid =
   { tmin = t ; tval = t ; tmax = t ; time = t ; tnbr = 1.0 ;
     success = if valid then 1.0 else 0.0 }
 
-let pqed r = ptime r.solver_time (VCS.is_valid r)
-let presult r = ptime r.prover_time (VCS.is_valid r)
+let pqed r = if VCS.is_valid r then ptime r.solver_time true else pzero
+let presult r = if VCS.is_valid r then ptime r.prover_time true else pzero
 let psolver r = ptime r.solver_time false
+let psmoked = { pzero with success = 1.0 }
 
 (* -------------------------------------------------------------------------- *)
 (* --- Global Stats                                                       --- *)
@@ -181,9 +182,7 @@ let results ~smoke prs =
       let cached = List.fold_left
           (fun c (_,r) -> if r.VCS.cached then succ c else c)
           0 passed in
-      let stucked = List.map
-          (fun (p,r) -> p, ptime r.prover_time true)
-          passed in
+      let stucked = List.map (fun (p,_) -> p,psmoked) passed in
       let solver = List.fold_left
           (fun t (_,r) -> t +. r.solver_time)
           0.0 passed in
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index ca000ced16280f15aba38e639191a32204a575b0..bc33fcaf7abca28614382f86138f80943e3ef136 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -150,28 +150,31 @@ module Pmap = Map.Make(P)
 
 type config = {
   valid : bool ;
-  timeout : int option ;
+  timeout : float option ;
   stepout : int option ;
 }
 
-let param f = let v = f() in if v>0 then Some v else None
-
-let current () = {
-  valid = false ;
-  timeout = param Wp_parameters.Timeout.get ;
-  stepout = param Wp_parameters.Steps.get ;
-}
+let current () =
+  let t = Wp_parameters.Timeout.get () in
+  let s = Wp_parameters.Steps.get () in
+  {
+    valid = false ;
+    timeout = if t > 0 then Some (float t) else None ;
+    stepout = if s > 0 then Some s else None ;
+  }
 
 let default = { valid = false ; timeout = None ; stepout = None }
 
 let get_timeout ?kf ~smoke = function
   | { timeout = None } ->
     if smoke
-    then Wp_parameters.SmokeTimeout.get ()
-    else begin match Option.map Wp_parameters.FctTimeout.find kf with
-      | exception Not_found | None -> Wp_parameters.Timeout.get ()
-      | Some timeout -> timeout
-    end
+    then float @@ Wp_parameters.SmokeTimeout.get ()
+    else
+      let t =
+        match Option.map Wp_parameters.FctTimeout.find kf with
+        | None | exception Not_found -> Wp_parameters.Timeout.get ()
+        | Some timeout -> timeout
+      in float t
   | { timeout = Some t } -> t
 
 let get_stepout = function
@@ -226,14 +229,14 @@ let configure r =
   let timeout =
     let t = r.prover_time in
     if t > 0.0 then
-      let timeout = Wp_parameters.Timeout.get() in
-      let margin = Wp_parameters.TimeExtra.get() + int_of_float (t +. 0.5) in
-      Some(max timeout margin)
+      let timeout = float @@ max 0 @@ Wp_parameters.Timeout.get() in
+      let margin = float @@ max 0 @@ Wp_parameters.TimeExtra.get () in
+      Some(timeout +. margin)
     else
       None in
   let stepout =
     if r.prover_steps > 0 && r.prover_time <= 0.0 then
-      let stepout = Wp_parameters.Steps.get () in
+      let stepout = max 0 @@ Wp_parameters.Steps.get () in
       let margin = 1000 in
       Some(max stepout margin)
     else None in
@@ -274,7 +277,7 @@ let no_result = result NoResult
 let valid = result Valid
 let invalid = result Invalid
 let unknown = result Unknown
-let timeout t = result ~time:(float t) Timeout
+let timeout t = result ~time:t Timeout
 let stepout n = result ~steps:n Stepout
 let computing kill = result (Computing kill)
 let failed ?pos msg = {
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 29098111ebd50b50a89f9a8723d8d4440768b5de..54bf33b6023467bd78ac40493cd0171e60ef1af0 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -62,7 +62,7 @@ val cmp_prover : prover -> prover -> int
 
 type config = {
   valid : bool ;
-  timeout : int option ;
+  timeout : float option ;
   stepout : int option ;
 }
 
@@ -70,8 +70,8 @@ val current : unit -> config (** Current parameters *)
 
 val default : config (** all None *)
 
-val get_timeout : ?kf:Kernel_function.t -> smoke:bool -> config -> int
-(** 0 means no-timeout *)
+val get_timeout : ?kf:Kernel_function.t -> smoke:bool -> config -> float
+(** 0.0 means no-timeout *)
 
 val get_stepout : config -> int (** 0 means no-stepout *)
 
@@ -102,7 +102,7 @@ val valid : result
 val invalid : result
 val unknown : result
 val stepout : int -> result
-val timeout : int -> result
+val timeout : float -> result
 val computing : (unit -> unit) -> result
 val failed : ?pos:Lexing.position -> string -> result
 val kfailed : ?pos:Lexing.position -> ('a,Format.formatter,unit,result) format4 -> 'a
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 97c5f8e56d2dc58082c26c07ff63c24b29a69591..d1bf09b57f5239934930e7e42e6da1ce9f2edaea 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1337,12 +1337,10 @@ See \texttt{-wp-interactive <mode>} option for details.
 \item[\tt -wp-(no)-proof-trace] asks for provers to output extra information
   on proved goals when available (default is: \texttt{no}).
 \item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
-  to the decision prover (defaults to 10 seconds).
+  to the decision prover (defaults to 2 seconds).
 \item[\tt -wp-fct-timeout <f1:t1,f2:t2,...>] customize the timeout for each
   specified function (\texttt{t1} for \texttt{f1}, \texttt{t2} for \texttt{f2},
   etc).
-\item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
-  (see \verb+-wp-smoke-tests+, defaults to 5 seconds).
 \item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking
   edited scripts with interactive provers (defaults to 30 seconds).
 \item[\tt -wp-(no)-script-on-stdout] displays generated proof scripts on stdout
diff --git a/src/plugins/wp/gui/GuiProver.ml b/src/plugins/wp/gui/GuiProver.ml
index 4e32d9956206c0d5fa3211aa9d359c9507a3221f..7f02b9f6fa7f86d59e6cc41cfde465b8d68df89b 100644
--- a/src/plugins/wp/gui/GuiProver.ml
+++ b/src/plugins/wp/gui/GuiProver.ml
@@ -89,7 +89,7 @@ class prover ~(console:Wtext.text) ~prover =
         let spinner = function None -> None | Some s -> Some s#get in
         let config = {
           VCS.valid = false ;
-          VCS.timeout = spinner timeout ;
+          VCS.timeout = Option.map float @@ spinner timeout ;
           VCS.stepout = spinner stepout ;
         } in
         let result wpo _prv _res = self#update wpo in
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 578de390af6709ba12624f183aa4751eb6c61990..65aefeed81d935d7eb0e181714a2775644d9e5ca 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -771,8 +771,9 @@ let pp_wp_parameters fmt =
     if spec <> [] && spec <> ["Typed"] then
       ( let descr = Factory.descr (Factory.parse spec) in
         Format.fprintf fmt " -wp-model '%s'" descr ) ;
+    let dt = Wp_parameters.Timeout.get_default () in
     let tm = Wp_parameters.Timeout.get () in
-    if tm <> 10 then Format.fprintf fmt " -wp-timeout %d" tm ;
+    if tm <> dt then Format.fprintf fmt " -wp-timeout %d" tm ;
     let st = Wp_parameters.Steps.get () in
     if st > 0 then Format.fprintf fmt " -wp-steps %d" st ;
     if not (Kernel.SignedOverflow.get ()) then
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index e714bb39358e99380c90ca6eedee2d6aa67bc322..48e506bbafd6257ea759e778f522e15383001b34 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -841,7 +841,7 @@ let () = Parameter_customize.set_group wp_prover
 module Timeout =
   Int(struct
     let option_name = "-wp-timeout"
-    let default = 10
+    let default = 2
     let arg_name = "n"
     let help =
       Printf.sprintf