diff --git a/.Makefile.lint b/.Makefile.lint
index c9c25b59427db306d25074f2aa3d54d1ece56144..69b506b6c4e6dcb894a746aed704839d6e5b8ee3 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -187,8 +187,6 @@ ML_LINT_KO+=src/libraries/utils/qstack.ml
 ML_LINT_KO+=src/libraries/utils/qstack.mli
 ML_LINT_KO+=src/libraries/utils/rangemap.ml
 ML_LINT_KO+=src/libraries/utils/rangemap.mli
-ML_LINT_KO+=src/libraries/utils/task.ml
-ML_LINT_KO+=src/libraries/utils/task.mli
 ML_LINT_KO+=src/libraries/utils/vector.ml
 ML_LINT_KO+=src/libraries/utils/vector.mli
 ML_LINT_KO+=src/libraries/utils/wto.ml
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 2f39dcfb9ebbc31493a48aca056321387c48e122..7750a6c5c9a1e6d78f4d6bc40b3c5bcea52576f3 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -79,19 +79,19 @@ sig
   val waiting : 'a t -> bool
 end =
 struct
-  
+
   type 'a t =
     | UNIT of 'a
     | WAIT of int * (coin -> 'a t)
     | YIELD of (coin -> 'a t)
 
   let unit a = UNIT a
-  
+
   let rec bind m f = match m with
     | UNIT a -> f a
     | WAIT(d,m) -> WAIT (d, fun c -> bind (m c) f)
     | YIELD m -> YIELD (fun c -> bind (m c) f)
-  
+
   let put c m = match m with
     | UNIT _ -> m
     | WAIT(_,f) | YIELD f -> f c
@@ -103,7 +103,7 @@ struct
     | Wait d -> WAIT(d,ping f)
     | Yield -> YIELD(ping f)
     | Return a -> UNIT a
-    
+
   let async f = YIELD (ping f)
 
   let rec wait = function
@@ -114,7 +114,7 @@ struct
   let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
 
   let waiting = function UNIT _ -> false | YIELD _ | WAIT _ -> true
-  
+
 end
 
 (* ------------------------------------------------------------------------ *)
@@ -141,20 +141,20 @@ let failed text =
 let bind = Monad.bind
 let async = Monad.async
 
-let sequence a k = 
+let sequence a k =
   Monad.bind a (function
       | Result r -> k r
       | Failed e -> Monad.unit (Failed e)
       | Timeout n -> Monad.unit (Timeout n)
       | Canceled -> Monad.unit Canceled)
-    
+
 let nop = return ()
 let nof _ = ()
 
 let later ?(canceled=nof) f x = Monad.yield
     begin fun coin ->
       try match coin with
-        | Coin -> f x 
+        | Coin -> f x
         | Kill -> canceled x ; Monad.unit Canceled
       with e -> raised e
     end
@@ -245,35 +245,35 @@ let start_command ~timeout ?time ?stdout ?stderr cmd args =
 let ping_command cmd coin =
   try
     match cmd.async () with
-    
+
     | Command.Not_ready kill ->
-        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
-            begin
-              set_time cmd (time_now -. cmd.time_start) ;
-              Kernel.debug ~dkey:Kernel.dkey_task "timeout '%s'" cmd.name ;
-              cmd.time_killed <- true ;
-              kill () ;
-            end ;
-          Wait 100
+      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
+          begin
+            set_time cmd (time_now -. cmd.time_start) ;
+            Kernel.debug ~dkey:Kernel.dkey_task "timeout '%s'" cmd.name ;
+            cmd.time_killed <- true ;
+            kill () ;
+          end ;
+        Wait 100
 
     | Command.Result (Unix.WEXITED s|Unix.WSIGNALED s|Unix.WSTOPPED s)
       when cmd.time_killed ->
-        set_chrono cmd ;
-        Kernel.debug ~dkey:Kernel.dkey_task "timeout '%s' [%d]" cmd.name s ;
-        Return (Timeout cmd.timeout)
+      set_chrono cmd ;
+      Kernel.debug ~dkey:Kernel.dkey_task "timeout '%s' [%d]" cmd.name s ;
+      Return (Timeout cmd.timeout)
 
     | Command.Result (Unix.WEXITED s) ->
-        set_chrono cmd ;
-        Kernel.debug ~dkey:Kernel.dkey_task "exit '%s' [%d]" cmd.name s ;
-        Return (Result s)
+      set_chrono cmd ;
+      Kernel.debug ~dkey:Kernel.dkey_task "exit '%s' [%d]" cmd.name s ;
+      Return (Result s)
 
     | Command.Result (Unix.WSIGNALED s|Unix.WSTOPPED s) ->
-        set_chrono cmd ;
-        Kernel.debug ~dkey:Kernel.dkey_task "signal '%s' [%d]" cmd.name s ;
-        Return Canceled
+      set_chrono cmd ;
+      Kernel.debug ~dkey:Kernel.dkey_task "signal '%s' [%d]" cmd.name s ;
+      Return Canceled
 
   with e ->
     set_chrono cmd ;
@@ -309,25 +309,25 @@ let retry_shared sh = function
 
 let ping_shared sh = function
   | Coin ->
-      begin match Monad.finished sh.shared with
-        | Some r ->
-            if retry_shared sh r then sh.shared <- todo sh.builder ;
-            Return r
-        | None -> sh.shared <- Monad.progress sh.shared ; Yield
+    begin match Monad.finished sh.shared with
+      | Some r ->
+        if retry_shared sh r then sh.shared <- todo sh.builder ;
+        Return r
+      | None -> sh.shared <- Monad.progress sh.shared ; Yield
+    end
+  | Kill ->
+    if sh.clients > 1 then
+      begin
+        sh.clients <- pred sh.clients ;
+        Return Canceled
       end
-  | Kill ->      
-      if sh.clients > 1 then
-        begin
-          sh.clients <- pred sh.clients ;
-          Return Canceled
-        end
-      else
-        ( if sh.clients = 1 then
-            begin
-              sh.clients <- 0 ;
-              sh.shared <- Monad.cancel sh.shared ;
-            end ;
-          Yield )
+    else
+      ( if sh.clients = 1 then
+          begin
+            sh.clients <- 0 ;
+            sh.shared <- Monad.cancel sh.shared ;
+          end ;
+        Yield )
 
 let share sh = todo
     begin fun () ->
@@ -338,7 +338,7 @@ let share sh = todo
 (* -------------------------------------------------------------------------- *)
 (* --- IDLE                                                               --- *)
 (* -------------------------------------------------------------------------- *)
-    
+
 let on_idle = ref
     (fun f -> try
         while f () do Extlib.usleep 50000 (* wait for 50ms *) done
@@ -505,4 +505,3 @@ let rec run_server server () =
 let launch server =
   if server.scheduled > server.terminated
   then ( fire server.start ; !on_idle (run_server server) )
-    
diff --git a/src/libraries/utils/task.mli b/src/libraries/utils/task.mli
index fb1f38ad0738bd4dcf55596ce6818ec4abcab7ad..355f2d9368ce02efc3bc9e3f028f157f3108bdb3 100644
--- a/src/libraries/utils/task.mli
+++ b/src/libraries/utils/task.mli
@@ -46,24 +46,24 @@ val pretty : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a status -
 (* ************************************************************************* *)
 
 val nop : unit task
-  (** The task that immediately returns unit *)
+(** The task that immediately returns unit *)
 
 val return : 'a -> 'a task
-  (** The task that immediately returns a result *)
+(** The task that immediately returns a result *)
 
 val raised : exn -> 'a task
-  (** The task that immediately fails with an exception *)
+(** The task that immediately fails with an exception *)
 
 val canceled : unit -> 'a task
-  (** The task that is immediately canceled *)
+(** The task that is immediately canceled *)
 
 val failed : ('a,Format.formatter,unit,'b task) format4 -> 'a
-  (** The task that immediately fails by raising a [Failure] exception.
-      Typically: [[let exit d : 'a task = failed "exit status %d" k]] *)
+(** The task that immediately fails by raising a [Failure] exception.
+    Typically: [[let exit d : 'a task = failed "exit status %d" k]] *)
 
 val call : ?canceled:('a -> unit) -> ('a -> 'b) -> 'a -> 'b task
-  (** The task that, when started, invokes a function and immediately
-      returns the result. *)
+(** The task that, when started, invokes a function and immediately
+    returns the result. *)
 
 val later : ?canceled:('a -> unit) -> ('a -> 'b task) -> 'a -> 'b task
 (** The task that, when started, compute a task to continue with. *)
@@ -72,31 +72,31 @@ val todo :  ?canceled:(unit -> unit) -> (unit -> 'a task) -> 'a task
 (** Specialized version of [later]. *)
 
 val status : 'a status -> 'a task
-  (** The task that immediately finishes with provided status *)
+(** The task that immediately finishes with provided status *)
 
 val bind : 'a task -> ('a status -> 'b task) -> 'b task
-  (** [bind t k] first runs [t]. Then, when [t] exit with status [s],
-      it starts task [k s].
+(** [bind t k] first runs [t]. Then, when [t] exit with status [s],
+    it starts task [k s].
 
-      <b>Remark:</b> If [t] was cancelled, [k s] is still evaluated, but
-      immediately canceled as well. This allows [finally]-like behaviors to
-      be implemented. To evaluate [k r] only when [t] terminates normally,
-      make use of the [sequence] operator. *)
+    <b>Remark:</b> If [t] was cancelled, [k s] is still evaluated, but
+    immediately canceled as well. This allows [finally]-like behaviors to
+    be implemented. To evaluate [k r] only when [t] terminates normally,
+    make use of the [sequence] operator. *)
 
 val sequence : 'a task -> ('a -> 'b task) -> 'b task
-  (** [sequence t k] first runs [t]. If [t] terminates with [Result r],
-      then task [k r] is started.
-      Otherwise, failure or cancelation of [t] is returned. *)
+(** [sequence t k] first runs [t]. If [t] terminates with [Result r],
+    then task [k r] is started.
+    Otherwise, failure or cancelation of [t] is returned. *)
 
 val job : 'a task -> unit task
 
 val finally : 'a task -> ('a status -> unit) -> 'a task
-  (** [finally t cb] runs task [t] and {i always} calls [cb s] when [t] exits
-      with status [s]. Then [s] is returned. If the callback [cb]
-      raises an exception, the returned status is emitted. *)
+(** [finally t cb] runs task [t] and {i always} calls [cb s] when [t] exits
+    with status [s]. Then [s] is returned. If the callback [cb]
+    raises an exception, the returned status is emitted. *)
 
 val callback : 'a task -> ('a status -> unit) -> unit task
-  (** Same as [finally] but the status of the task is discarded. *)
+(** Same as [finally] but the status of the task is discarded. *)
 
 type 'a async =
   | Yield (** give up the control *)
@@ -136,10 +136,10 @@ val command :
   ?stdout:Buffer.t ->
   ?stderr:Buffer.t ->
   string -> string array -> int task
-  (** Immediately launch a system-process.
-      Default timeout is [0], which means no-timeout at all.
-      Standard outputs are discarded unless optional buffers are provided.
-      To make the task start later, simply use [todo (command ...)]. *)
+(** Immediately launch a system-process.
+    Default timeout is [0], which means no-timeout at all.
+    Standard outputs are discarded unless optional buffers are provided.
+    To make the task start later, simply use [todo (command ...)]. *)
 
 (* ************************************************************************* *)
 (** {2 Shared Tasks}
@@ -147,7 +147,7 @@ val command :
     When two tasks [A] and [B] share a common sub-task [S],
     cancelling [A] will make [B] fail either. To prevent this, it is
     necessary to make [S] {i shareable} and to use two distinct {i
-    instances} of [S] in [A] and [B]. 
+    instances} of [S] in [A] and [B].
 
     Shared tasks manage the number of their instance and actually run
     or cancel a unique task on demand. In particular, shared tasks can
@@ -156,17 +156,17 @@ val command :
     @since Oxygen-20120901 *)
 (* ************************************************************************* *)
 
-type 'a shared 
-  (** Shareable tasks. *)
+type 'a shared
+(** Shareable tasks. *)
 
-val shared : descr:string -> retry:bool -> (unit -> 'a task) -> 'a shared 
+val shared : descr:string -> retry:bool -> (unit -> 'a task) -> 'a shared
 (** Build a shareable task.  The build function is called whenever a new
     instance is required but no shared instance task is actually running.
     Interrupted tasks (by Cancel or Timeout) are retried for further
     instances. If the task failed, it can be re-launch if [retry] is [true].
     Otherwise, further instances will return [Failed] status. *)
 
-val share : 'a shared -> 'a task 
+val share : 'a shared -> 'a task
 (** New instance of shared task. *)
 
 (* ************************************************************************* *)
@@ -181,11 +181,11 @@ val progress : thread -> bool
 (** Make the thread progress and return [true] if still running *)
 
 val is_running : thread -> bool
-(** Don't make the thread progress, just returns [true] 
+(** Don't make the thread progress, just returns [true]
     if not terminated or not started yet *)
-  
+
 val run : thread -> unit
-(** Runs one single task in the background. 
+(** Runs one single task in the background.
     Typically using [on_idle]. *)
 
 (* ************************************************************************* *)
@@ -209,23 +209,23 @@ val server :
   ?stages:int ->
   ?procs:int ->
   unit -> server
-  (** Creates a server of commands.
-      @param stages number of queues in the server.
-      Stage 0 tasks are issued first. Default is 1.
-      @param procs maximum number of running tasks. Default is 4. *)
+(** Creates a server of commands.
+    @param stages number of queues in the server.
+    Stage 0 tasks are issued first. Default is 1.
+    @param procs maximum number of running tasks. Default is 4. *)
 
 val spawn : server -> ?pool:pool -> ?stage:int -> thread -> unit
-  (** Schedules a task on the server.
-      The task is not immediately started. *)
+(** Schedules a task on the server.
+    The task is not immediately started. *)
 
 val launch : server -> unit
-  (** Starts the server if not running yet *)
+(** Starts the server if not running yet *)
 
 val cancel_all : server -> unit
-  (** Cancel all scheduled tasks *)
+(** Cancel all scheduled tasks *)
 
 val set_procs : server -> int -> unit
-  (** Adjusts the maximum number of running process. *)
+(** Adjusts the maximum number of running process. *)
 
 val on_server_activity : server -> (unit -> unit) -> unit
 (** Idle server callback *)
@@ -249,8 +249,7 @@ val waiting : server -> int option
 (* ************************************************************************* *)
 
 val on_idle : ((unit -> bool) -> unit) ref
-  (** Typically modified by GUI.
-      [!on_idle f] should repeatedly calls [f] until it returns [false].
-      Default implementation rely on [Unix.sleep 1] and [Db.progress].
-      See also [Gtk_helper] module implementation. *)
-
+(** Typically modified by GUI.
+    [!on_idle f] should repeatedly calls [f] until it returns [false].
+    Default implementation rely on [Unix.sleep 1] and [Db.progress].
+    See also [Gtk_helper] module implementation. *)
diff --git a/src/plugins/qed/export_altergo.ml b/src/plugins/qed/export_altergo.ml
index 52864b8b16668ab498ef8c25f9eeebb6ff98629a..70087ff2d4c3fa0d889c221010c5b280ec1db11a 100644
--- a/src/plugins/qed/export_altergo.ml
+++ b/src/plugins/qed/export_altergo.ml
@@ -114,8 +114,8 @@ struct
       method op_add (_:amode) = Assoc "+"
       method op_sub (_:amode) = Assoc "-"
       method op_mul (_:amode) = Assoc "*"
-      method op_div = function Aint -> Call "comp_div" | Areal -> Op "/"
-      method op_mod = function Aint -> Call "comp_mod" | Areal -> Call "rmod"
+      method op_div = function Aint -> Call "div" | Areal -> Op "/"
+      method op_mod = function Aint -> Call "mod" | Areal -> Call "rmod"
 
       method op_eq cmode _amode =
         match cmode with
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 46d91b13189d1f9670263c60c7a74b57391745d0..83554c5172952d432128bc89186a4fca41796c8b 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,11 +20,15 @@
 #   <Prover>: prover
 ###############################################################################
 
-- WP	      [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
+- TIP         [2019/09/17] Using all selected Why-3 provers for proof search
+- Gui         [2019/09/17] Updated panel for provers, models, cache, etc.
+- WP          [2019/09/12] New cache mechanism for why3 provers, see -wp-cache option
+-! WP         [2019/09/17] Deprecated native alt-ergo & coq output, see -wp-prover option
+-! WP         [2019/07/05] -wp-prover <p> now defaults to <why3:p> (including default alt-ergo)
+-! WP         [2019/07/05] Use native Why3 API (now requires why3 at compile time)
 - WP          [2019/06/27] Improving Cint simplifier and quantifier introduction
-o WP          [2019/06/27] Using the new API of Qed
-o Qed         [2019/06/27] Changes into the API in order to get a more secure way to manipulate quantifiers and binding
-- Qed         [2019/05/09] Transforms some boolean quantifications into let constructs
+o Qed         [2019/06/27] More secure API for quantifier management
+- Qed         [2019/05/09] Transform (some) boolean quantifications into variable assignments
 
 ##########################
 Plugin WP 19.0 (Potassium)
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 7974c19d95c5687637e2efec6d721f0dde723458..9bba13a5711c45c9e4157907840b19482b49de5a 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -24,7 +24,7 @@
 (* ---  Prover List in Configuration                                    --- *)
 (* ------------------------------------------------------------------------ *)
 
-class enabled key =
+class provers key =
   object(self)
     inherit [Why3.Whyconf.Sprover.t] Wutil.selector Why3.Whyconf.Sprover.empty
 
@@ -63,7 +63,7 @@ class enabled key =
         let selection = List.fold_left
             (fun acc e ->
                match Why3Provers.find_opt e with
-               | None-> acc
+               | None -> acc
                | Some p -> Why3.Whyconf.Sprover.add p acc)
             settings cmdline
         in
@@ -79,7 +79,7 @@ class enabled key =
 
 class dp_chooser
     ~(main:Design.main_window_extension_points)
-    ~(enabled:enabled)
+    ~(provers:provers)
   =
   let dialog = new Wpane.dialog
     ~title:"Why3 Provers"
@@ -123,7 +123,7 @@ class dp_chooser
       end
 
     method private apply () =
-      enabled#set
+      provers#set
         (Why3.Whyconf.Mprover.map_filter
            (function
              | true -> Some ()
@@ -132,7 +132,7 @@ class dp_chooser
 
     method run () =
       let dps = Why3Provers.provers_set () in
-      let sel = enabled#get in
+      let sel = provers#get in
       selected <- Why3.Whyconf.Mprover.merge
           (fun _ avail enab ->
              match avail, enab with
@@ -156,70 +156,3 @@ class dp_chooser
   end
 
 (* ------------------------------------------------------------------------ *)
-(* ---  WP Prover Switch Panel                                          --- *)
-(* ------------------------------------------------------------------------ *)
-
-type mprover =
-  | NONE
-  | ERGO
-  | COQ
-  | WHY of Why3Provers.t
-
-class dp_button () =
-  let render = function
-    | NONE -> "(none)"
-    | ERGO -> "Alt-Ergo (native)"
-    | COQ -> "Coq (native)"
-    | WHY p when Why3Provers.has_shortcut p "alt-ergo" ->
-        "Alt-Ergo (why3)"
-    | WHY dp -> Why3Provers.title dp in
-  let select = function
-    | ERGO -> VCS.NativeAltErgo
-    | COQ -> VCS.NativeCoq
-    | NONE -> VCS.Qed
-    | WHY p -> VCS.Why3 p in
-  let rec import = function
-    | [] -> ERGO
-    | spec::others ->
-        match VCS.prover_of_name spec with
-        | None | Some VCS.Qed -> NONE
-        | Some (VCS.NativeAltErgo|VCS.Tactical) -> ERGO
-        | Some VCS.NativeCoq -> COQ
-        | Some (VCS.Why3 p) ->
-            if Why3.Whyconf.Sprover.mem p (Why3Provers.provers_set ())
-            then WHY p
-            else import others
-  in
-  let items = [ NONE ; ERGO ; COQ ] in
-  let button = new Widget.menu ~default:ERGO ~render ~items () in
-  object(self)
-    method coerce = button#coerce
-    method widget = (self :> Widget.t)
-    method set_enabled = button#set_enabled
-    method set_visible = button#set_visible
-    val mutable dps = Why3.Whyconf.Sprover.empty
-
-    method update () =
-      (* called in polling mode *)
-      begin
-        let avl = Why3Provers.provers_set () in
-        if Why3.Whyconf.Sprover.equal avl dps then
-          begin
-            dps <- avl ;
-            let dps = Why3.Whyconf.Sprover.elements dps in
-            let items = [NONE;ERGO] @ List.map (fun p -> WHY p) dps @ [COQ] in
-            button#set_items items
-          end ;
-        let cur = Wp_parameters.Provers.get () |> import in
-        if cur <> button#get then button#set cur ;
-      end
-
-    initializer button#connect
-        (fun s ->
-           let p = select s in
-           let p = VCS.name_of_prover p in
-           Wp_parameters.Provers.set [p]
-        )
-  end
-
-(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/GuiConfig.mli
index 4e068822df192ed6d57cb98d9320a85a988f334a..d812b88b23b8ae9a4780693ba75105d2401e8be9 100644
--- a/src/plugins/wp/GuiConfig.mli
+++ b/src/plugins/wp/GuiConfig.mli
@@ -24,17 +24,13 @@
 (* ---  WP Provers Configuration Panel                                  --- *)
 (* ------------------------------------------------------------------------ *)
 
-class enabled : string -> [Why3.Whyconf.Sprover.t] Widget.selector
+class provers : string -> [Why3.Whyconf.Sprover.t] Widget.selector
 
 class dp_chooser :
   main:Design.main_window_extension_points ->
-  enabled:enabled ->
+  provers:provers ->
   object
     method run : unit -> unit (** Edit enabled provers *)
   end
 
-class dp_button : unit ->
-  object
-    inherit Widget.widget
-    method update : unit -> unit
-  end
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 6e45285f6923815571a9abe055761eea9119ff85..e88783bd3830cc6ae6295d6a397b186c69b72fd3 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -84,7 +84,7 @@ class rformat =
 (* --- Goal Panel                                                         --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane (enabled : GuiConfig.enabled) =
+class pane (gprovers : GuiConfig.provers) =
   let icon = new Widget.image GuiProver.no_status in
   let status = new Widget.label () in
   let text = new Wtext.text () in
@@ -114,6 +114,7 @@ class pane (enabled : GuiConfig.enabled) =
   let iformat = new iformat in
   let rformat = new rformat in
   let strategies = new GuiTactic.strategies () in
+  let native = List.mem "native:alt-ergo" (Wp_parameters.Provers.get ()) in
   object(self)
 
     val mutable state : state = Empty
@@ -135,11 +136,15 @@ class pane (enabled : GuiConfig.enabled) =
             Config.config_float ~key:"GuiGoal.palette" ~default:0.8 content
           );
         layout#populate (Wbox.panel ~top:toolbar content#widget) ;
-        provers <-
-          VCS.([ new GuiProver.prover ~console:text ~prover:NativeAltErgo ] @
-               List.map
-                 (fun dp -> new GuiProver.prover text (VCS.Why3 dp))
-                 (Why3.Whyconf.Sprover.elements enabled#get)) ;
+        let native_ergo =
+          if native then [
+            new GuiProver.prover ~console:text ~prover:VCS.NativeAltErgo
+          ] else [] in
+        let why3_provers =
+          List.map
+            (fun dp -> new GuiProver.prover ~console:text ~prover:(VCS.Why3 dp))
+            (Why3.Whyconf.Sprover.elements gprovers#get) in
+        provers <- native_ergo @ why3_provers ;
         List.iter (fun p -> palette#add_tool p#tool) provers ;
         palette#add_tool strategies#tool ;
         Strategy.iter strategies#register ;
@@ -149,11 +154,11 @@ class pane (enabled : GuiConfig.enabled) =
              tactics <- gtac :: tactics ;
              palette#add_tool gtac#tool) ;
         tactics <- List.rev tactics ;
-        self#register_provers enabled#get;
+        self#register_provers gprovers#get;
         printer#on_selection (fun () -> self#update) ;
         scripter#on_click self#goto ;
         scripter#on_backtrack self#backtrack ;
-        enabled#connect self#register_provers ;
+        gprovers#connect self#register_provers ;
         delete#connect (fun () -> self#interrupt ProofEngine.reset) ;
         cancel#connect (fun () -> self#interrupt ProofEngine.cancel) ;
         forward#connect (fun () -> self#forward) ;
@@ -264,12 +269,17 @@ class pane (enabled : GuiConfig.enabled) =
           in
           autofocus#set mode ; self#update
 
+    method private provers =
+      (if native then [ VCS.NativeAltErgo ] else []) @
+      (List.map (fun dp -> VCS.Why3 dp)
+         (Why3.Whyconf.Sprover.elements gprovers#get))
+
     method private play_script =
       match state with
       | Proof p ->
           ProofEngine.reset p ;
           ProverScript.spawn
-            ~provers:[ VCS.NativeAltErgo ]
+            ~provers:self#provers
             ~result:
               (fun wpo prv res ->
                  text#printf "[%a] %a : %a@."
@@ -583,12 +593,12 @@ class pane (enabled : GuiConfig.enabled) =
               VCS.pp_prover prv Wpo.pp_title wpo VCS.pp_result res
           end
         ~success:(fun _ _ -> Wutil.later self#commit)
-        ~pool provers
+        ~pool (List.map (fun dp -> VCS.BatchMode , dp) provers)
 
     method private fork proof fork =
       Wutil.later
         begin fun () ->
-          let provers = VCS.[ BatchMode, NativeAltErgo ] in
+          let provers = self#provers in
           let pool = Task.pool () in
           ProofEngine.iter (self#schedule pool provers) fork ;
           let server = ProverTask.server () in
diff --git a/src/plugins/wp/GuiGoal.mli b/src/plugins/wp/GuiGoal.mli
index 4e64a05983eb9346d8a1e3fa97c4bd7f5abaf7c8..fd60b80fa866f48cc812eca08b1de154985a3bad 100644
--- a/src/plugins/wp/GuiGoal.mli
+++ b/src/plugins/wp/GuiGoal.mli
@@ -24,7 +24,7 @@
 (* --- PO Details View                                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane : GuiConfig.enabled ->
+class pane : GuiConfig.provers ->
   object
 
     method select : Wpo.t option -> unit
diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 5148d14d0ef7c4dbf97bceb1deed67cee863d22b..83c43b08dcb585f208c705e3bd4a45e8fe74d726 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -72,7 +72,7 @@ let render_prover_result p =
         end
     | { verdict=r } , _ -> icon_of_verdict r
 
-class pane (enabled:GuiConfig.enabled) =
+class pane (gprovers:GuiConfig.provers) =
   let model = new model in
   let list = new Wtable.list ~headers:true ~rules:true model#coerce in
   object(self)
@@ -121,8 +121,9 @@ class pane (enabled:GuiConfig.enabled) =
         List.iter
           (fun (vcs,column) ->
              match vcs with
-             | VCS.Why3 p when not (Why3.Whyconf.Sprover.mem p dps) ->
-                 ignore (list#view#remove_column column)
+             | VCS.Why3 p ->
+                 column#set_visible (Why3.Whyconf.Sprover.mem p dps) ;
+                 (* ignore (list#view#remove_column column) *)
              | _ -> ()
           ) provers ;
         (* Installing Missing Columns *)
@@ -147,11 +148,16 @@ class pane (enabled:GuiConfig.enabled) =
         ignore (list#add_column_text ~title:"Model" [] render) ;
         List.iter
           self#create_prover
-          [ VCS.Qed ; VCS.Tactical ; VCS.NativeAltErgo ; VCS.NativeCoq ] ;
+          [ VCS.Qed ; VCS.Tactical ] ;
+        let prv = Wp_parameters.Provers.get () in
+        if List.mem "native:alt-ergo" prv then
+          self#create_prover VCS.NativeAltErgo ;
+        if List.mem "native:coq" prv then
+          self#create_prover VCS.NativeCoq ;
         ignore (list#add_column_empty) ;
         list#set_selection_mode `MULTIPLE ;
-        enabled#connect self#configure ;
-        self#configure enabled#get ;
+        gprovers#connect self#configure ;
+        self#configure gprovers#get ;
       end
 
     method private on_cell f w c = f w (self#prover_of_column c)
diff --git a/src/plugins/wp/GuiList.mli b/src/plugins/wp/GuiList.mli
index e3db77b28d1fae378c63ab34ba7e434fc22d8cfb..7b34f43d5db14f6cc3080193182ca80fbc2ea9e9 100644
--- a/src/plugins/wp/GuiList.mli
+++ b/src/plugins/wp/GuiList.mli
@@ -24,7 +24,7 @@
 (* --- PO List View                                                       --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane : GuiConfig.enabled ->
+class pane : GuiConfig.provers ->
   object
 
     method show : Wpo.t -> unit
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 57257f3a473f37f47275477c31d6aff6a4437b8a..eed9d0dbb42755fd2a0035f35b4032694a03fb20 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -91,6 +91,7 @@ class behavior
     ~(clear : Widget.button)
     ~(card : card Widget.selector)
     ~(list : GuiList.pane)
+    ~(provers : GuiConfig.provers)
     ~(goal : GuiGoal.pane)
     ~(source : GuiSource.highlighter)
     ~(popup : GuiSource.popup)
@@ -238,24 +239,28 @@ class behavior
           let server = ProverTask.server () in
           Task.spawn server thread ;
           Task.launch server in
-        match prover with
-        | VCS.Tactical ->
-            begin
-              match mode , ProverScript.get w with
-              | (None | Some VCS.BatchMode) , `Script ->
-                  schedule (ProverScript.prove ~success w)
-              | _ ->
-                  card#set `Goal ;
-                  clear#set_enabled false ;
-                  self#navigator true (Some w) ;
-            end
-        | _ ->
-            let mode = match mode , prover with
-              | Some m , _ -> m
-              | None , VCS.NativeCoq -> VCS.EditMode
-              | None , VCS.NativeAltErgo -> VCS.FixMode
-              | _ -> VCS.BatchMode in
-            schedule (Prover.prove w ~mode ~result prover)
+        if not (VCS.is_valid (Wpo.get_result w VCS.Qed)) &&
+           not (VCS.is_computing (Wpo.get_result w prover))
+        then
+          match prover with
+          | VCS.Tactical ->
+              begin
+                match mode , ProverScript.get w with
+                | (None | Some VCS.BatchMode) , `Script ->
+                    schedule (ProverScript.prove ~success w)
+                | _ ->
+                    card#set `Goal ;
+                    clear#set_enabled false ;
+                    self#navigator true (Some w) ;
+              end
+          | _ ->
+              let mode = match mode , prover with
+                | Some m , _ -> m
+                | None , VCS.NativeCoq -> VCS.EditMode
+                | None , VCS.NativeAltErgo -> VCS.FixMode
+                | _ -> VCS.BatchMode in
+              schedule (Prover.prove w ~mode ~result prover) ;
+              refresh w
       end
 
     method private clear () =
@@ -376,12 +381,42 @@ class behavior
         card#connect (fun _ -> self#details) ;
         scope#connect self#set_scope ;
         popup#on_click self#set_selection ;
-        popup#on_prove (GuiPanel.run_and_prove main) ;
+        popup#on_prove (GuiPanel.run_and_prove main provers) ;
         clear#connect self#clear ;
       end
 
   end
 
+(* -------------------------------------------------------------------------- *)
+(* --- Model Info for Variables                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+let model_varinfo :
+  GMenu.menu GMenu.factory ->
+  Design.main_window_extension_points ->
+  button:int -> Pretty_source.localizable -> unit =
+  fun _menu main ~button item ->
+  let open Pretty_source in
+  let open Cil_types in
+  match item with
+  | PLval(Some kf, _ , (Var x,NoOffset))
+  | PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset))
+    when button=1 ->
+      let init = WpStrategy.is_main_init kf in
+      let acc = RefUsage.get ~kf ~init x in
+      let model = match acc with
+        | RefUsage.NoAccess -> "any"
+        | RefUsage.ByValue -> "'var'"
+        | RefUsage.ByRef -> "'ref'"
+        | RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype
+          -> "'caveat'"
+        | _ -> "'typed'"
+      in
+      main#pretty_information
+        "Is is accessed as %t and fits in %s wp-model@."
+        (RefUsage.print x acc) model ;
+  | _ -> ()
+
 (* -------------------------------------------------------------------------- *)
 (* --- Make Panel and Extend Frama-C GUI                                  --- *)
 (* -------------------------------------------------------------------------- *)
@@ -393,9 +428,9 @@ let make (main : main_window_extension_points) =
     (* --- Provers                                                            --- *)
     (* -------------------------------------------------------------------------- *)
 
-    let enabled = new GuiConfig.enabled "wp.enabled" in
+    let provers = new GuiConfig.provers "wp.provers" in
 
-    let dp_chooser = new GuiConfig.dp_chooser ~main ~enabled in
+    let dp_chooser = new GuiConfig.dp_chooser ~main ~provers in
 
     (* -------------------------------------------------------------------------- *)
     (* --- Focus Bar                                                          --- *)
@@ -419,7 +454,7 @@ let make (main : main_window_extension_points) =
         (index :> widget) ;
         (next :> widget) ;
       ] in
-    let provers = new Widget.button ~label:"Provers..." () in
+    let pvrs = new Widget.button ~label:"Provers..." () in
     let clear = new Widget.button ~label:"Clear" ~icon:`DELETE () in
     let focusbar = GPack.hbox ~spacing:0 () in
     begin
@@ -427,8 +462,8 @@ let make (main : main_window_extension_points) =
       focusbar#pack ~padding:20 ~expand:false scope#coerce ;
       focusbar#pack ~padding:20 ~expand:false filter#coerce ;
       focusbar#pack ~from:`END ~expand:false clear#coerce ;
-      focusbar#pack ~from:`END ~expand:false provers#coerce ;
-      provers#connect dp_chooser#run ;
+      focusbar#pack ~from:`END ~expand:false pvrs#coerce ;
+      pvrs#connect dp_chooser#run ;
     end ;
 
     (* -------------------------------------------------------------------------- *)
@@ -448,8 +483,8 @@ let make (main : main_window_extension_points) =
     (* -------------------------------------------------------------------------- *)
 
     let book = new Wpane.notebook ~default:`List () in
-    let list = new GuiList.pane enabled in
-    let goal = new GuiGoal.pane enabled in
+    let list = new GuiList.pane provers in
+    let goal = new GuiGoal.pane provers in
     begin
       book#add `List list#coerce ;
       book#add `Goal goal#coerce ;
@@ -471,7 +506,7 @@ let make (main : main_window_extension_points) =
     let filter = (filter :> _ Widget.selector) in
     let behavior = new behavior ~main
       ~next ~prev ~index ~scope ~filter ~clear
-      ~list ~card ~goal ~source ~popup in
+      ~list ~provers ~card ~goal ~source ~popup in
     GuiPanel.on_reload behavior#reload ;
     GuiPanel.on_update behavior#update ;
 
@@ -487,6 +522,7 @@ let make (main : main_window_extension_points) =
     ignore (main#lower_notebook#append_page ~tab_label panel#coerce) ;
     main#register_source_highlighter source#highlight ;
     main#register_source_selector popup#register ;
+    main#register_source_selector model_varinfo ;
 
     GuiPanel.register ~main
       ~configure_provers:dp_chooser#run ;
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 253b9ef08efdbfa0fd33dfee36d2b4f4d1268ee6..c8e6c9759eecbe636134f440610674ab36cca227 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -63,8 +63,14 @@ let wp_rte_generated s =
         not mem
       else false
 
+let spawn provers vcs =
+  if not (Bag.is_empty vcs) then
+    let provers = Why3.Whyconf.Sprover.elements provers#get in
+    VC.command ~provers ~tip:true vcs
+
 let run_and_prove
     (main:Design.main_window_extension_points)
+    (provers:GuiConfig.provers)
     (selection:GuiSource.selection)
   =
   begin
@@ -72,9 +78,9 @@ let run_and_prove
       begin
         match selection with
         | S_none -> raise Stop
-        | S_fun kf -> VC.(command (generate_kf kf))
-        | S_prop ip -> VC.(command (generate_ip ip))
-        | S_call s -> VC.(command (generate_call s.s_stmt))
+        | S_fun kf -> spawn provers (VC.generate_kf kf)
+        | S_prop ip -> spawn provers (VC.generate_ip ip)
+        | S_call s -> spawn provers (VC.generate_call s.s_stmt)
       end ;
       if wp_rte_generated selection then
         main#redisplay ()
@@ -97,6 +103,7 @@ class model_selector (main : Design.main_window_extension_points) =
   let r_typed  = memory#add_radio ~label:"Typed Memory Model" ~value:TYPED () in
   let c_casts  = new Widget.checkbox ~label:"Unsafe casts" () in
   let c_byref  = new Widget.checkbox ~label:"Reference Arguments" () in
+  let c_ctxt   = new Widget.checkbox ~label:"Context Arguments (Caveat)" () in
   let c_cint   = new Widget.checkbox ~label:"Machine Integers" () in
   let c_cfloat = new Widget.checkbox ~label:"Floating Points" () in
   let m_label  = new Widget.label ~style:`Title () in
@@ -108,6 +115,7 @@ class model_selector (main : Design.main_window_extension_points) =
         dialog#add_row r_typed#coerce ;
         dialog#add_row c_casts#coerce ;
         dialog#add_row c_byref#coerce ;
+        dialog#add_row c_ctxt#coerce ;
         dialog#add_row c_cint#coerce ;
         dialog#add_row c_cfloat#coerce ;
         dialog#add_row m_label#coerce ;
@@ -117,6 +125,7 @@ class model_selector (main : Design.main_window_extension_points) =
         memory#on_event self#connect ;
         c_casts#on_event self#connect ;
         c_byref#on_event self#connect ;
+        c_ctxt#on_event self#connect ;
         c_cint#on_event self#connect ;
         c_cfloat#on_event self#connect ;
         dialog#on_value `APPLY self#update ;
@@ -132,6 +141,7 @@ class model_selector (main : Design.main_window_extension_points) =
          | Hoare -> memory#set HOARE
          | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)) ;
         c_byref#set (s.mvar = Ref) ;
+        c_ctxt#set (s.mvar = Caveat) ;
         c_cint#set (s.cint = Cint.Machine) ;
         c_cfloat#set (s.cfloat = Cfloat.Float) ;
       end
@@ -145,12 +155,16 @@ class model_selector (main : Design.main_window_extension_points) =
                      (if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
       in {
         mheap = m ;
-        mvar = if c_byref#get then Ref else Var ;
+        mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;
         cint = if c_cint#get then Cint.Machine else Cint.Natural ;
         cfloat = if c_cfloat#get then Cfloat.Float else Cfloat.Real ;
       }
 
-    method connect () = m_label#set_text (Factory.descr self#get)
+    method connect () =
+      begin
+        m_label#set_text (Factory.descr self#get) ;
+        c_byref#set_enabled (not c_ctxt#get) ;
+      end
 
     method run =
       begin
@@ -166,31 +180,8 @@ class model_selector (main : Design.main_window_extension_points) =
 (* ---  WP Panel                                                        --- *)
 (* ------------------------------------------------------------------------ *)
 
-let wp_dir = ref (Sys.getcwd())
-
-let wp_script () =
-  let file = Gtk_helper.select_file
-      ~title:"Script File for Coq proofs"
-      ~dir:wp_dir ~filename:"wp.script" ()
-  in
-  match file with
-  | Some f -> Wp_parameters.Script.set f
-  | None -> ()
-
-let wp_update_model label () =
-  let s = Factory.parse (Wp_parameters.Model.get ()) in
-  label#set_text (Factory.descr s)
-
-let wp_configure_model main label () =
-  begin
-    (new model_selector main)#run ;
-    wp_update_model label () ;
-  end
-
-let wp_update_script label () =
-  let file = Wp_parameters.Script.get () in
-  let text = if file = "" then "(None)" else Filename.basename file in
-  label#set_text text
+let wp_configure_model main () =
+  (new model_selector main)#run
 
 let wp_panel
     ~(main:Design.main_window_extension_points)
@@ -200,70 +191,19 @@ let wp_panel
   let demon = Gtk_form.demon () in
   let packing = vbox#pack in
 
-  let form = new Wpane.form () in
-  (* Model Row *)
-  let model_cfg = new Widget.button
-    ~label:"Model..." ~tooltip:"Configure WP Model" () in
-  let model_lbl = GMisc.label ~xalign:0.0 () in
-  Gtk_form.register demon (wp_update_model model_lbl) ;
-  model_cfg#connect (wp_configure_model main model_lbl) ;
-  form#add_label_widget model_cfg#coerce ;
-  form#add_field model_lbl#coerce ;
-  (* Script Row *)
-  let script_cfg = new Widget.button
-    ~label:"Script..." ~tooltip:"Load/Save User Scripts file" () in
-  let script_lbl = GMisc.label ~xalign:0.0 () in
-  Gtk_form.register demon (wp_update_script script_lbl) ;
-  script_cfg#connect wp_script ;
-  form#add_label_widget script_cfg#coerce ;
-  form#add_field script_lbl#coerce ;
-  (* Prover Row *)
-  let prover_cfg = new Widget.button
-    ~label:"Provers..." ~tooltip:"Detect WP Provers" () in
-  prover_cfg#connect configure_provers ;
-  form#add_label_widget prover_cfg#coerce ;
-  let prover_menu = new GuiConfig.dp_button () in
-  form#add_field prover_menu#coerce ;
-  Gtk_form.register demon prover_menu#update ;
-  (* End Form *)
-  packing form#coerce ;
-
-  let options = GPack.hbox ~spacing:16 ~packing () in
-
-  Gtk_form.check ~label:"RTE"
-    ~tooltip:"Generates RTE guards for WP"
-    ~packing:options#pack
-    Wp_parameters.RTE.get Wp_parameters.RTE.set demon ;
-
-  Gtk_form.check ~label:"Split"
-    ~tooltip:"Splits conjunctions into sub-goals"
-    ~packing:options#pack
-    Wp_parameters.Split.get Wp_parameters.Split.set demon ;
-
-  Gtk_form.check ~label:"Trace"
-    ~tooltip:"Reports proof information from provers"
-    ~packing:options#pack
-    Wp_parameters.ProofTrace.get Wp_parameters.ProofTrace.set demon ;
-
-  let control = GPack.table ~columns:2 ~col_spacings:8 ~rows:4 ~packing () in
+  let control = GPack.table ~columns:2 ~col_spacings:8 ~rows:2 ~packing () in
   let addcontrol line col w = control#attach ~left:(col-1) ~top:(line-1) ~expand:`NONE w in
 
-  Gtk_form.label ~text:"Steps" ~packing:(addcontrol 1 1) () ;
-  Gtk_form.spinner ~lower:0 ~upper:100000
-    ~tooltip:"Search steps for alt-ergo prover"
-    ~packing:(addcontrol 1 2)
-    Wp_parameters.Steps.get Wp_parameters.Steps.set demon ;
-
-  Gtk_form.label ~text:"Timeout" ~packing:(addcontrol 3 1) () ;
+  Gtk_form.label ~text:"timeout" ~packing:(addcontrol 1 2) () ;
   Gtk_form.spinner ~lower:0 ~upper:100000
     ~tooltip:"Timeout for proving one proof obligation"
-    ~packing:(addcontrol 3 2)
+    ~packing:(addcontrol 1 1)
     Wp_parameters.Timeout.get Wp_parameters.Timeout.set demon ;
 
-  Gtk_form.label ~text:"Process" ~packing:(addcontrol 4 1) () ;
+  Gtk_form.label ~text:"process" ~packing:(addcontrol 2 2) () ;
   Gtk_form.spinner ~lower:1 ~upper:32
     ~tooltip:"Maximum number of parallel running provers"
-    ~packing:(addcontrol 4 2)
+    ~packing:(addcontrol 2 1)
     Wp_parameters.Procs.get
     (fun n ->
        Wp_parameters.Procs.set n ;
@@ -271,6 +211,28 @@ let wp_panel
        (* to make server procs updated is server exists *)
     ) demon ;
 
+  let hbox = GPack.hbox ~packing () in
+
+  let model_cfg = new Widget.button
+    ~label:"Model..." ~tooltip:"Configure WP Model" () in
+  model_cfg#connect (wp_configure_model main) ;
+  hbox#pack model_cfg#coerce ;
+
+  let prover_cfg = new Widget.button
+    ~label:"Provers..." ~tooltip:"Detect WP Provers" () in
+  prover_cfg#connect configure_provers ;
+  hbox#pack prover_cfg#coerce ;
+
+  Gtk_form.menu [
+    "No Cache" ,    ProverWhy3.NoCache ;
+    "Update" ,  ProverWhy3.Update ;
+    "Cleanup" , ProverWhy3.Cleanup ;
+    "Rebuild" , ProverWhy3.Rebuild ;
+    "Replay" ,  ProverWhy3.Replay ;
+    "Offline" , ProverWhy3.Offline ;
+  ] ~packing:hbox#pack ~tooltip:"Proof Cache Mode"
+    ProverWhy3.get_mode ProverWhy3.set_mode demon ;
+
   let pbox = GPack.hbox ~packing ~show:false () in
   let progress = GRange.progress_bar ~packing:(pbox#pack ~expand:true ~fill:true) () in
   let cancel = GButton.button ~packing:(pbox#pack ~expand:false) ~stock:`STOP () in
diff --git a/src/plugins/wp/GuiPanel.mli b/src/plugins/wp/GuiPanel.mli
index 25219a0c506570dcf0aa9d6af42d008c5e78e4ab..83642c83d9cadbc98c2f73137365f10414b3c68f 100644
--- a/src/plugins/wp/GuiPanel.mli
+++ b/src/plugins/wp/GuiPanel.mli
@@ -27,7 +27,8 @@ val reload : unit -> unit
 val on_reload : (unit -> unit) -> unit
 
 val run_and_prove :
-  Design.main_window_extension_points -> GuiSource.selection -> unit
+  Design.main_window_extension_points ->
+  GuiConfig.provers -> GuiSource.selection -> unit
 
 val register :
   main:Design.main_window_extension_points ->
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index be6cd3a9ebf68135da4081ae8e91bb78509f107b..7e2b91afb6f9eb66305c9baee77613b743034ab0 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -440,7 +440,6 @@ let spawn
               ~depth ~width ~backtrack ~auto
               ~start ~progress ~result ~success wpo)
 
-
 let search
     ?(depth = 0) ?(width = 0) ?(backtrack = 0) ?(auto = []) ?(provers = [])
     ?(progress = skip2) ?(result = skip3) ?(success = skip2)
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index 95ac91b54a78f1b936e758e5604d9945eb848792..a2e6ea942697d83376ea55d968f1922ede00a6b9 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -292,9 +292,14 @@ let getprocs = function Some n -> n | None -> Wp_parameters.Procs.get ()
 let server ?procs () =
   match !server with
   | Some s ->
-      Task.set_procs s (getprocs procs) ; s
+      let np = getprocs procs in
+      Task.set_procs s np ;
+      Why3Provers.set_procs np ;
+      s
   | None ->
-      let s = Task.server ~procs:(getprocs procs) () in
+      let np = getprocs procs in
+      let s = Task.server ~procs:np () in
+      Why3Provers.set_procs np ;
       Task.on_server_stop s Proof.savescripts ;
       server := Some s ; s
 
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index bd4235548ac9a83f57cdaae89a3f19ca2459ccd2..30bd663bb6d935ecc6b42ab11ad07cf18bf0def0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -34,6 +34,9 @@ let option_import = LogicBuiltins.create_option
     (fun ~driver_dir:_ x -> x)
     "why3" "import"
 
+let why3_failure msg =
+  Pretty_utils.ksfprintf failwith msg
+
 module Env = WpContext.Index(struct
     include Datatype.Unit
     type key = unit
@@ -81,7 +84,7 @@ let get_ls ~cnv ~f ~l ~p =
     try
       Why3.Theory.ns_find_ls th.th_export p
     with Not_found ->
-      Wp_parameters.fatal "The symbol %a can't be found in %a.%s"
+      why3_failure "The symbol %a can't be found in %a.%s"
         Why3.Pp.(print_list dot string) p
         Why3.Pp.(print_list dot string) f l
   in
@@ -93,7 +96,7 @@ let get_ts ~cnv ~f ~l ~p =
     try
       Why3.Theory.ns_find_ts th.th_export p
     with Not_found ->
-      Wp_parameters.fatal "The type %a can't be found in %a.%s"
+      why3_failure "The type %a can't be found in %a.%s"
         Why3.Pp.(print_list dot string) p
         Why3.Pp.(print_list dot string) f l
   in
@@ -239,12 +242,12 @@ let rec of_tau ~cnv (t:Lang.F.tau) =
       let s = name_of_adt adt in
       match Why3.Theory.(ns_find_ts (get_namespace cnv.th) (cut_path s)) with
       | ts -> Some (Why3.Ty.ty_app ts (List.map (fun e -> Why3.Opt.get (of_tau ~cnv e)) l))
-      | exception Not_found -> Wp_parameters.fatal "Can't find type [%s] in why3 namespace" s
+      | exception Not_found ->
+          why3_failure "Can't find type '%s' in why3 namespace" s
     end
   | Tvar i -> Some (Why3.Ty.ty_var (tvar i))
   | Record _ ->
-      Wp_parameters.not_yet_implemented "Type %a not yet convertible"
-        Lang.F.pp_tau t
+      why3_failure "Type %a not (yet) convertible" Lang.F.pp_tau t
 
 let rec full_trigger = function
   | Qed.Engine.TgAny -> false
@@ -265,7 +268,7 @@ let rec of_trigger ~cnv t =
   | Qed.Engine.TgAny -> assert false (** absurd: filter by full_triggers *)
   | Qed.Engine.TgVar v -> begin
       try Lang.F.Tmap.find (Lang.F.e_var v) cnv.subst
-      with Not_found -> Wp_parameters.fatal "Unbound variable %a" Lang.F.pp_var v
+      with Not_found -> why3_failure "Unbound variable %a" Lang.F.pp_var v
     end
   | Qed.Engine.TgGet(m,k) ->
       t_app ~cnv ~f:["map"] ~l:"Map" ~p:["get"] [of_trigger cnv m;of_trigger cnv k]
@@ -276,7 +279,7 @@ let rec of_trigger ~cnv t =
       | F_call s ->
           let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
           Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger cnv e) l)
-      | _ -> Wp_parameters.not_yet_implemented "lfun in triggers"
+      | _ -> why3_failure "can not convert extented calls in triggers"
     end
   | TgProp (f,l) ->
       begin
@@ -284,7 +287,7 @@ let rec of_trigger ~cnv t =
         | F_call s ->
             let ls = Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) in
             Why3.Term.t_app_infer ls (List.map (fun e -> of_trigger cnv e) l)
-        | _ -> Wp_parameters.not_yet_implemented "lfun in triggers"
+        | _ -> why3_failure "can not convert extented calls in triggers"
       end
 
 let rec of_term ~cnv expected t : Why3.Term.term =
@@ -445,17 +448,18 @@ let rec of_term ~cnv expected t : Why3.Term.term =
           | ls, _ ->
               coerce ~cnv sort expected $
               t_app ls l (of_tau cnv sort)
-          | exception Not_found -> Wp_parameters.fatal "Can't find [%s] in why3 namespace" s
+          | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
         in
         let apply_from_ns' s l =
           apply_from_ns s (List.map (fun e -> of_term' cnv e) l)
         in
         match lfun_name f, expected with
         | F_call s, _ -> apply_from_ns' s l sort
-        | Qed.Engine.F_subst _, _ -> Wp_parameters.not_yet_implemented "lfun with subst"
+        | Qed.Engine.F_subst _, _ ->
+            why3_failure "Driver link with subst not yet implemented"
         | Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
             let rec aux = function
-              | [] -> Wp_parameters.fatal "Empty application"
+              | [] -> why3_failure "Empty application"
               | [a] -> of_term cnv expected a
               | a::l ->
                   apply_from_ns s [of_term' cnv a; aux l] sort
@@ -463,7 +467,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
             aux l
         | Qed.Engine.F_right s, _ ->
             let rec aux = function
-              | [] -> Wp_parameters.fatal "Empty application"
+              | [] -> why3_failure "Empty application"
               | [a] -> of_term cnv expected a
               | a::l ->
                   apply_from_ns s [aux l;of_term' cnv a] sort
@@ -479,14 +483,14 @@ let rec of_term ~cnv expected t : Why3.Term.term =
         | Qed.Engine.F_bool_prop (s,_), Bool | Qed.Engine.F_bool_prop (_,s), Prop ->
             apply_from_ns' s l expected
         | Qed.Engine.F_bool_prop (_,_), _ ->
-            Wp_parameters.fatal "badly expected type %a for term %a"
+            why3_failure "badly expected type %a for term %a"
               Lang.F.pp_tau expected Lang.F.pp_term t
       end
     | Rget(a,f), _ , _ -> begin
         let s = Lang.name_of_field f in
         match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) with
         | ls -> Why3.Term.t_app ls [of_term' cnv a] (of_tau cnv expected)
-        | exception Not_found -> Wp_parameters.fatal "Can't find [%s] in why3 namespace" s
+        | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
       end
     | Rdef(l), Data(Comp c,_) , _ -> begin
         (* l is already sorted by field *)
@@ -495,7 +499,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
         | ls ->
             let l = List.map (fun (_,t) -> of_term' cnv t) l in
             Why3.Term.t_app ls l (of_tau cnv expected)
-        | exception Not_found -> Wp_parameters.fatal "Can't find [%s] in why3 namespace" s
+        | exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
       end
     | (Rdef _, Data ((Mtype _|Mrecord (_, _)|Atype _), _), _)
     | (Rdef _, (Prop|Bool|Int|Real|Tvar _|Array (_, _)), _)
@@ -521,7 +525,7 @@ let rec of_term ~cnv expected t : Why3.Term.term =
     | (Bind (Lambda, _, _), _, _)
     | Apply _ , _, _
     | Rdef _, Record _, _ ->
-        Wp_parameters.not_yet_implemented
+        why3_failure
           "Can't convert to why3 the qed term %a of type %a"
           Lang.F.pp_term t Lang.F.pp_tau sort
   in
@@ -594,7 +598,7 @@ let convert cnv expected t =
 let mk_binders cnv l =
   List.fold_left (fun (cnv,lets) v ->
       match of_tau cnv (Lang.F.tau_of_var v) with
-      | None -> Wp_parameters.fatal "Quantification on prop"
+      | None -> why3_failure "Quantification on prop"
       | Some ty ->
           let x = Why3.Ident.id_fresh (Lang.F.Var.basename v) in
           let x = Why3.Term.create_vsymbol x ty in
@@ -676,7 +680,7 @@ class visitor (ctx:context) c =
 
     method add_import ?was thy =
       match Str.split_delim regexp_dot thy with
-      | [] -> Wp_parameters.fatal "empty import option"
+      | [] -> why3_failure "[driver] empty import option"
       | l ->
           let file, thy = Why3.Lists.chop_last l in
           self#add_import_use file thy (Why3.Opt.get_def thy was) ~import:true
@@ -723,8 +727,8 @@ class visitor (ctx:context) c =
         | [file;lib;name] ->
             copy_file file;
             self#add_import_file_as [filenoext file] lib name;
-        | _ -> Wp_parameters.failure ~current:false
-                 "Driver: why3.file %S not recognized (theory %s)"
+        | _ -> why3_failure
+                 "[driver] incorrect why3.file %S for library '%s'"
                  opt thy
       in
       let iter_import opt =
@@ -732,8 +736,8 @@ class visitor (ctx:context) c =
             match Str.split_delim regexp_col import with
             | [ th ] -> self#add_import th
             | [ th ; was ] -> self#add_import ~was th
-            | _ -> Wp_parameters.failure ~current:false
-                     "Driver: why3.import %S not recognized (theory %s)"
+            | _ -> why3_failure
+                     "[driver] incorrect why3.file %S for library '%s'"
                      opt thy
           ) (Str.split regexp_com opt)
       in
@@ -931,10 +935,7 @@ class visitor (ctx:context) c =
                 ctx.th <- Why3.Theory.add_decl ~warn:false ctx.th decl
           end
         | Inductive _dl ->
-            Wp_parameters.not_yet_implemented "inductive"
-            (* engine#declare_signature fmt
-             *   d.d_lfun (List.map F.tau_of_var d.d_params) Logic.Prop;
-             * List.iter self#on_dlemma dl *)
+            why3_failure "inductive definitions not yet implemented"
       end
 
   end
@@ -1029,6 +1030,62 @@ let prover_task prover task =
 
 let altergo_step_limit = Str.regexp "^Steps limit reached:"
 
+type prover_call = {
+  prover : Why3Provers.t ;
+  call : Why3.Call_provers.prover_call ;
+  steps : int option ;
+  timeover : float option ;
+  mutable interrupted : bool ;
+  mutable killed : bool ;
+}
+
+let ping_prover_call p =
+  match Why3.Call_provers.query_call p.call with
+  | NoUpdates
+  | ProverStarted ->
+      let () = match p.timeover with
+        | None -> ()
+        | Some timeout ->
+            let time = Unix.time () in
+            if time > timeout then
+              begin
+                Wp_parameters.debug ~dkey "Hard Kill (late why3server timeout)" ;
+                p.interrupted <- true ;
+                Why3.Call_provers.interrupt_call p.call ;
+              end
+      in Task.Wait 100
+  | InternalFailure exn ->
+      let msg = Format.asprintf "@[<hov 2>%a@]"
+          Why3.Exn_printer.exn_printer exn in
+      Task.Return (Task.Result (VCS.failed msg))
+  | ProverInterrupted -> Task.(Return Canceled)
+  | ProverFinished _ when p.killed -> Task.(Return Canceled)
+  | ProverFinished pr ->
+      let r =
+        match pr.pr_answer with
+        | Timeout -> VCS.timeout (int_of_float 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"
+        | StepLimitExceeded -> VCS.result ?steps:p.steps VCS.Stepout
+        | Unknown _ -> VCS.unknown
+        | _ when p.interrupted -> VCS.timeout (int_of_float pr.pr_time)
+        | Failure s -> VCS.failed s
+        | HighFailure ->
+            let alt_ergo_hack =
+              p.prover.prover_name = "Alt-Ergo" &&
+              Str.string_match altergo_step_limit pr.pr_output 0
+            in
+            if alt_ergo_hack then VCS.result ?steps:p.steps VCS.Stepout
+            else VCS.failed "Unknown error"
+      in
+      Wp_parameters.debug ~dkey
+        "@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
+        Why3.Whyconf.print_prover p.prover
+        (Why3.Call_provers.print_prover_result) pr
+        VCS.pp_result r;
+      Task.Return (Task.Result r)
+
 let call_prover ~timeout ~steplimit drv prover prover_config task =
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
   let limit =
@@ -1045,39 +1102,22 @@ let call_prover ~timeout ~steplimit drv prover prover_config task =
     Why3.Whyconf.print_prover prover
     (Why3.Opt.get_def (-1) timeout)
     (Why3.Opt.get_def (-1) steps);
-  let ping _ (* why3 seems not to be able to kill a started prover *) =
-    match Why3.Call_provers.query_call call with
-    | NoUpdates
-    | ProverStarted -> Task.Yield
-    | InternalFailure exn ->
-        let msg = Format.asprintf "%a" Why3.Exn_printer.exn_printer exn in
-        Task.Return (Task.Result (VCS.failed msg))
-    | ProverInterrupted ->
-        Task.Return (Task.Result (VCS.failed "interrupted"))
-    | ProverFinished pr ->
-        let r = match pr.pr_answer with
-          | Timeout -> VCS.timeout (int_of_float 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"
-          | StepLimitExceeded -> VCS.result ?steps VCS.Stepout
-          | Unknown _ -> VCS.unknown
-          | Failure s -> VCS.failed s
-          | HighFailure ->
-              let alt_ergo_hack =
-                prover.prover_name = "Alt-Ergo" &&
-                Str.string_match altergo_step_limit pr.pr_output 0
-              in
-              if alt_ergo_hack then VCS.result ?steps VCS.Stepout
-              else VCS.failed "Unknown error"
-        in
-        Wp_parameters.debug ~dkey
-          "@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
-          Why3.Whyconf.print_prover prover
-          (* why3 1.3 (Why3.Call_provers.print_prover_result ~json_model:false) pr *)
-          (Why3.Call_provers.print_prover_result) pr
-          VCS.pp_result r;
-        Task.Return (Task.Result r)
+  let timeover = match timeout with
+    | None -> None | Some tlimit ->
+        let started = Unix.time () in
+        Some (started +. 2.0 +. float tlimit) in
+  let pcall = {
+    call ; prover ;
+    killed = false ;
+    interrupted = false ;
+    steps ; timeover ;
+  } in
+  let ping = function
+    | Task.Kill ->
+        pcall.killed <- true ;
+        Why3.Call_provers.interrupt_call call ;
+        Task.Yield
+    | Task.Coin -> ping_prover_call pcall
   in
   Task.async ping
 
@@ -1098,7 +1138,7 @@ let get_miss () = !miss
 let get_removed () = !removed
 
 let mark_cache ~mode hash =
-  if mode = Cleanup then Hashtbl.replace cleanup hash ()
+  if mode = Cleanup || !Config.is_gui then Hashtbl.replace cleanup hash ()
 
 let cleanup_cache ~mode =
   if mode = Cleanup && (!hits > 0 || !miss > 0) then
@@ -1116,8 +1156,8 @@ let cleanup_cache ~mode =
                  end
           ) (Sys.readdir dir) ;
     with Unix.Unix_error _ as exn ->
-      Wp_parameters.failure "Can not cleanup cache (%s)"
-        (Printexc.to_string exn)
+      Wp_parameters.warning ~current:false
+        "Can not cleanup cache (%s)" (Printexc.to_string exn)
 
 (* -------------------------------------------------------------------------- *)
 (* --- Cache Management                                                   --- *)
@@ -1136,6 +1176,14 @@ let parse_mode ~origin ~fallback = function
         "Unknown %s mode %S (use %s instead)" origin m fallback ;
       raise Not_found
 
+let mode_name = function
+  | NoCache -> "none"
+  | Update -> "update"
+  | Replay -> "replay"
+  | Rebuild -> "rebuild"
+  | Offline -> "offline"
+  | Cleanup -> "cleanup"
+
 module MODE = WpContext.StaticGenerator(Datatype.Unit)
     (struct
       type key = unit
@@ -1155,6 +1203,7 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
     end)
 
 let get_mode = MODE.get
+let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
 
 let task_hash wpo drv prover task =
   lazy
@@ -1223,8 +1272,8 @@ let get_cache_result ~mode hash =
           mark_cache ~mode hash ;
           Json.load_file file |> ProofScript.result_of_json
         with err ->
-          Wp_parameters.failure ~once:true "invalid cache entry (%s)"
-            (Printexc.to_string err) ;
+          Wp_parameters.warning ~current:false ~once:true
+            "invalid cache entry (%s)" (Printexc.to_string err) ;
           VCS.no_result
 
 let set_cache_result ~mode hash prover result =
@@ -1239,8 +1288,8 @@ let set_cache_result ~mode hash prover result =
         ProofScript.json_of_result (VCS.Why3 prover) result
         |> Json.save_file file
       with err ->
-        Wp_parameters.failure ~once:true "can not update cache (%s)"
-          (Printexc.to_string err)
+        Wp_parameters.warning ~current:false ~once:true
+          "can not update cache (%s)" (Printexc.to_string err)
 
 let is_trivial (t : Why3.Task.task) =
   let goal = Why3.Task.task_goal_fmla t in
@@ -1250,7 +1299,7 @@ let is_trivial (t : Why3.Task.task) =
 (* --- Prove WPO                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let prove ?timeout ?steplimit ~prover wpo =
+let build_proof_task ?timeout ?steplimit ~prover wpo () =
   try
     WpContext.on_context (Wpo.get_context wpo)
       begin fun () ->
@@ -1263,7 +1312,7 @@ let prove ?timeout ?steplimit ~prover wpo =
         then Task.return VCS.no_result (* Only generate *)
         else
           let drv , config , task = prover_task prover task in
-          if false && is_trivial task then
+          if is_trivial task then
             Task.return VCS.valid
           else
             let mode = get_mode () in
@@ -1287,20 +1336,24 @@ let prove ?timeout ?steplimit ~prover wpo =
                     Task.return result
                   end
                 else
-                  begin
-                    incr miss ;
-                    Task.finally
-                      (call_prover ~timeout ~steplimit drv prover config task)
-                      (function
-                        | Task.Result result when VCS.is_verdict result ->
-                            set_cache_result ~mode hash prover result
-                        | _ -> ())
-                  end
+                  Task.finally
+                    (call_prover ~timeout ~steplimit drv prover config task)
+                    begin function
+                      | Task.Result result when VCS.is_verdict result ->
+                          incr miss ;
+                          set_cache_result ~mode hash prover result
+                      | _ -> ()
+                    end
       end ()
   with exn ->
-    let bt = Printexc.get_raw_backtrace () in
-    Wp_parameters.fatal "Error in why3:%a@.%s@."
-      Why3.Exn_printer.exn_printer exn
-      (Printexc.raw_backtrace_to_string bt)
+    if Wp_parameters.has_dkey dkey_api then
+      Wp_parameters.fatal "[Why3 Error] %a@\n%s"
+        Why3.Exn_printer.exn_printer exn
+        Printexc.(raw_backtrace_to_string @@ get_raw_backtrace ())
+    else
+      Task.failed "[Why3 Error] %a" Why3.Exn_printer.exn_printer exn
+
+let prove ?timeout ?steplimit ~prover wpo =
+  Task.later (build_proof_task ?timeout ?steplimit ~prover wpo) ()
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index e107c669a1514fc99be25823adee3dc9c7eaf2c6..4ab0212732d894a162b841c184622930a62aeef1 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -31,6 +31,8 @@ val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
 (** Return NoResult if it is already proved by Qed *)
 
 type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
+
+val set_mode : mode -> unit
 val get_mode : unit -> mode
 val get_hits : unit -> int
 val get_miss : unit -> int
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 894b937dc129c5c34a7458f0d21ee0b5eaeb36b7..0f0291f96b028d234ccf00561f7e3e37fd93ac6d 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -844,6 +844,8 @@ let get ?kf ?(init=false) vi =
 
 let compute () = ignore (usage ())
 
+let print x m fmt = Access.pretty x fmt m
+
 let dump () =
   Log.print_on_output
     begin fun fmt ->
diff --git a/src/plugins/wp/RefUsage.mli b/src/plugins/wp/RefUsage.mli
index ca3e2cf74ef0cbda1d88b548749f8cc55de78e01..9fa8852d6c99279a3855cafa3c04af876720c1a6 100644
--- a/src/plugins/wp/RefUsage.mli
+++ b/src/plugins/wp/RefUsage.mli
@@ -38,5 +38,6 @@ val get : ?kf:kernel_function -> ?init:bool -> varinfo -> access
 
 val iter: ?kf:kernel_function -> ?init:bool -> (varinfo -> access -> unit) -> unit
 
+val print : varinfo -> access -> Format.formatter -> unit
 val dump : unit -> unit
 val compute : unit -> unit
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index eed3642e3f00269f91036d8c5abf4f3e67e930cc..506deb1860a12366d1ff070bb8dddc9df185de77 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -96,6 +96,7 @@ let prove = Prover.prove
 let spawn = Prover.spawn ~delayed:true
 
 let server = ProverTask.server
-let command vcs = Register.do_wp_proofs_iter (fun f -> Bag.iter f vcs)
+let command ?provers ?tip vcs =
+  Register.do_wp_proofs_iter ?provers ?tip (fun f -> Bag.iter f vcs)
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index eb916875fb6b2123a2790410784a9a9a7a493ae4..630be0e0e5025b1e9ac3055eae7afd5466531815 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -98,7 +98,9 @@ val server : ?procs:int -> unit -> Task.server
     The returned server is global to Frama-C, but the number of parallel task
     allowed will be updated to fit the [~procs] or command-line options. *)
 
-val command : t Bag.t -> unit
-(** Run the provers with the command-line interface *)
+val command : ?provers:Why3.Whyconf.prover list -> ?tip:bool -> t Bag.t -> unit
+(** Run the provers with the command-line interface.
+    If [~provers] is set, it is used for computing the list of provers to spawn.
+    If [~tip] is set, it is used to compute the script execution mode. *)
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index adeabe58e0df3e40b73e6b6169db14ecca0ab92d..f71051092d0debef538974948b08cd8ad48d8de3 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -42,22 +42,21 @@ type mode =
   | EditMode  (* Edit then check scripts *)
   | FixMode   (* Try check script, then edit script on non-success *)
 
-type language =
-  | L_why3
-  | L_coq
-  | L_altergo
-
 let prover_of_name = function
   | "" | "none" -> None
   | "qed" | "Qed" -> Some Qed
-  | "alt-ergo" | "altgr-ergo" -> Some (Why3 (Why3Provers.find "alt-ergo"))
-  | "native-alt-ergo" | "native-altgr-ergo"
+  | "native-alt-ergo" (* for wp-reports *)
   | "native:alt-ergo" | "native:altgr-ergo"
-    -> Some NativeAltErgo
-  | "coq" | "coqide"
-  | "native-coq" | "native-coqide"
-  | "native:coq" | "native:coqide"
-    -> Some NativeCoq
+    ->
+      Wp_parameters.warning ~once:true ~current:false
+        "native support for alt-ergo is deprecated, use why3 instead" ;
+      Some NativeAltErgo
+  | "native-coq" (* for wp-reports *)
+  | "native:coq" | "native:coqide" | "native:coqedit"
+    ->
+      Wp_parameters.warning ~once:true ~current:false
+        "native support for coq is deprecated, use tip instead" ;
+      Some NativeCoq
   | "script" -> Some Tactical
   | "tip" -> Some Tactical
   | "why3" -> Some (Why3 { Why3.Whyconf.prover_name = "why3";
@@ -69,6 +68,11 @@ let prover_of_name = function
       | Some s' -> Some (Why3 (Why3Provers.find s'))
       | None -> Some (Why3 (Why3Provers.find s))
 
+let mode_of_prover_name = function
+  | "native:coqedit" -> EditMode
+  | "native:coqide" | "native:altgr-ergo" -> FixMode
+  | _ -> BatchMode
+
 let name_of_prover = function
   | Why3 s -> "why3:" ^ (Why3Provers.print s)
   | NativeAltErgo -> "alt-ergo"
@@ -109,24 +113,6 @@ let filename_for_prover = function
   | Qed -> "Qed"
   | Tactical -> "Tactical"
 
-let language_of_prover = function
-  | Why3 _ -> L_why3
-  | NativeCoq -> L_coq
-  | NativeAltErgo -> L_altergo
-  | Qed | Tactical -> L_why3
-
-let language_of_prover_name = function
-  | "" | "none" -> None
-  | "alt-ergo" | "altgr-ergo" -> Some L_altergo
-  | "coq" | "coqide" -> Some L_coq
-  | _ -> Some L_why3
-
-let mode_of_prover_name = function
-  | "coqedit" -> EditMode
-  | "coqide" | "native-coqide" | "native:coqide"
-  | "altgr-ergo" | "tactical" -> FixMode
-  | _ -> BatchMode
-
 let is_auto = function
   | Qed | NativeAltErgo | Why3 _ -> true
   | Tactical | NativeCoq -> false
@@ -158,11 +144,6 @@ let pp_prover fmt = function
   | Qed -> Format.fprintf fmt "Qed"
   | Tactical -> Format.pp_print_string fmt "Tactical"
 
-let pp_language fmt = function
-  | L_altergo -> Format.pp_print_string fmt "Alt-Ergo"
-  | L_coq -> Format.pp_print_string fmt "Coq"
-  | L_why3 -> Format.pp_print_string fmt "Why3"
-
 let pp_mode fmt m = Format.pp_print_string fmt (title_of_mode m)
 
 module P = struct type t = prover let compare = cmp_prover end
@@ -226,7 +207,8 @@ let is_verdict r = match r.verdict with
   | Valid | Checked | Unknown | Invalid | Timeout | Stepout | Failed -> true
   | NoResult | Computing _ -> false
 
-let is_valid r = r.verdict = Valid
+let is_valid = function { verdict = Valid } -> true | _ -> false
+let is_computing = function { verdict=Computing _ } -> true | _ -> false
 
 let configure r =
   let valid = (r.verdict = Valid) in
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 873c4c621140519c1278ce5a85ebc936b9c3a5e4..ef4284710e81be4e5c59f1ab3b2f09d921758a84 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -38,25 +38,17 @@ type mode =
   | EditMode  (* Edit then check scripts *)
   | FixMode   (* Try check script, then edit script on non-success *)
 
-type language =
-  | L_why3
-  | L_coq
-  | L_altergo
-
 module Pset : Set.S with type elt = prover
 module Pmap : Map.S with type key = prover
 
-val language_of_prover : prover -> language
 val name_of_prover : prover -> string
 val title_of_prover : prover -> string
 val filename_for_prover : prover -> string
 val prover_of_name : string -> prover option
-val language_of_prover_name: string -> language option
 val mode_of_prover_name : string -> mode
 val title_of_mode : mode -> string
 
 val pp_prover : Format.formatter -> prover -> unit
-val pp_language : Format.formatter -> language -> unit
 val pp_mode : Format.formatter -> mode -> unit
 
 val cmp_prover : prover -> prover -> int
@@ -119,6 +111,7 @@ val result : ?cached:bool -> ?solver:float -> ?time:float -> ?steps:int -> verdi
 val is_auto : prover -> bool
 val is_verdict : result -> bool
 val is_valid: result -> bool
+val is_computing: result -> bool
 val configure : result -> config
 val autofit : result -> bool (** Result that fits the default configuration *)
 
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index b9af04531e7018dc748abe783bb119d752f94672..a7bb783256673119bd9d380d123424676444f0aa 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -35,6 +35,8 @@ let cfg = lazy
 let version = Why3.Config.version
 let config () = Lazy.force cfg
 
+let set_procs = Why3.Controller_itp.set_session_max_tasks
+
 let configure =
   let todo = ref true in
   begin fun () ->
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index a68eeb567d8caab7089bd8d82af71bfbfb7c1a25..d08bf2d0337eb3f917644bacabc24d738aa61309 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -23,6 +23,7 @@
 val version : string
 val config : unit -> Why3.Whyconf.config
 val configure : unit -> unit
+val set_procs : int -> unit
 
 type t = Why3.Whyconf.prover
 
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 3f93fa21f7a9e0628163176d4edf3f9325aa2618..e9b9477243ea904b45bf416c80c619b64a3a8375 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -511,7 +511,6 @@ let do_list_scheduled_result () =
 (* ------------------------------------------------------------------------ *)
 
 type mode = {
-  mutable why3ide : bool ;
   mutable tactical : bool ;
   mutable update : bool ;
   mutable depth : int ;
@@ -585,7 +584,7 @@ let dump_strategies =
                )))
 
 let default_mode () = {
-  why3ide = false ; tactical = false ; update=false ; provers = [] ;
+  tactical = false ; update=false ; provers = [] ;
   depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
 }
 
@@ -668,11 +667,18 @@ let do_update_session mode iter =
           Wp_parameters.result "Updated session with %d new script%s to complete." f s );
     end
 
-let do_wp_proofs_iter iter =
+let do_wp_proofs_iter ?provers ?tip iter =
   let mode = default_mode () in
   compute_provers ~mode ;
   compute_auto ~mode ;
-  let spawned = mode.why3ide || mode.tactical || mode.provers <> [] in
+  begin match provers with None -> () | Some prvs ->
+    mode.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+  end ;
+  begin match tip with None -> () | Some tip ->
+    mode.tactical <- tip ;
+    mode.update <- tip ;
+  end ;
+  let spawned = mode.tactical || mode.provers <> [] in
   begin
     if spawned then do_list_scheduled iter ;
     spawn_wp_proofs_iter ~mode iter ;
@@ -905,15 +911,16 @@ let do_prover_detect () =
     else
       let open Why3.Whyconf in
       let shortcuts = get_prover_shortcuts (Why3Provers.config ()) in
+      let print_prover_shortcuts_for fmt p =
+        Why3.Wstdlib.Mstr.iter
+          (fun name p' -> if Prover.equal p p' then
+              Format.fprintf fmt "%s|" name)
+          shortcuts in
       List.iter
         (fun p ->
-           Wp_parameters.result "Prover %10s %-10s %s [%t%a]"
-             p.prover_name p.prover_version p.prover_altern
-             (fun fmt ->
-                Why3.Wstdlib.Mstr.iter
-                  (fun name p' -> if Prover.equal p p' then
-                      Format.fprintf fmt "%s," name)
-                  shortcuts)
+           Wp_parameters.result "Prover %10s %-6s [%a%a]"
+             p.prover_name p.prover_version
+             print_prover_shortcuts_for p
              print_prover_parseable_format p
         ) provers
 
diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c
index fd61fe0481e4059843c2383436fa1e56ba1325ff..570d50707379b44f32c2c6f1cb71d2723f202a35 100644
--- a/src/plugins/wp/tests/wp_acsl/classify_float.c
+++ b/src/plugins/wp/tests/wp_acsl/classify_float.c
@@ -1,7 +1,7 @@
 /* run.config_qualif
    OPT: -wp-prover alt-ergo
-   OPT: -wp-prover why3:alt-ergo
-   OPT: -wp-prover coq -wp-coq-script tests/wp_acsl/classify_float.script
+   OPT: -wp-prover native:alt-ergo
+   OPT: -wp-prover native:coq -wp-coq-script tests/wp_acsl/classify_float.script
    OPT: -wp-model real
  */
 
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
index 1c0f3f3f388045d820787e6f640a6480a9742c5d..f8c7592ac59b554bbfc9ab43c599bd34fcbc795d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle
@@ -2,16 +2,17 @@
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 3 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_InfN_not_finite : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_InfP_not_finite : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_NaN_not_finite : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_InfN_not_finite : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_InfP_not_finite : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_NaN_not_finite : Valid
 [wp] Proved goals:    3 / 3
-  Qed:               0 
-  Alt-Ergo 2.0.0:    3
+  Qed:             0 
+  Alt-Ergo:        3
 [wp] Report in:  'tests/wp_acsl/oracle_qualif/classify_float.1.report.json'
 [wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json'
 -------------------------------------------------------------
 Axiomatics          WP     Alt-Ergo        Total   Success
-Lemma               -       3 (4..16)        3       100%
+Lemma               -      -  (4..16)        3       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
index 7ddef8f6c1163e7ec87114454f625be52a78fe2f..b0a7fe5b78141a5798c6f78db7c26bd5c789b058 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 3 goals scheduled
 [wp] [Coq] Goal typed_lemma_InfN_not_finite : Saved script
 [wp] [Coq (Native)] Goal typed_lemma_InfN_not_finite : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
index e0c64dbd19c005bd7baa08847082f1b9199a1e47..64863ed1b30a21d7b49779d2a2414d5090217709 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.0.report.json
@@ -1,49 +1,34 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 34, "valid": 34,
-                                          "rank": 0 },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 34, "valid": 34 },
                  "qed": { "total": 8, "valid": 8 },
-                 "wp:main": { "total": 42, "valid": 42, "rank": 0 } },
+                 "wp:main": { "total": 42, "valid": 42 } },
   "wp:functions": { "f": { "f_ensures_f1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_f0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o4": { "qed": { "total": 1,
                                                       "valid": 1 },
                                              "wp:main": { "total": 1,
@@ -53,107 +38,73 @@
                                              "wp:main": { "total": 1,
                                                           "valid": 1 } },
                            "f_ensures_o2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_o0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a4": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_a0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i9": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i6": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i5": { "qed": { "total": 1,
                                                       "valid": 1 },
                                              "wp:main": { "total": 1,
@@ -163,23 +114,17 @@
                                              "wp:main": { "total": 1,
                                                           "valid": 1 } },
                            "f_ensures_i3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_i0": { "qed": { "total": 1,
                                                       "valid": 1 },
                                              "wp:main": { "total": 1,
@@ -189,59 +134,43 @@
                                              "wp:main": { "total": 1,
                                                           "valid": 1 } },
                            "f_ensures_p8": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p7": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p6": { "qed": { "total": 1,
                                                       "valid": 1 },
                                              "wp:main": { "total": 1,
                                                           "valid": 1 } },
                            "f_ensures_p5": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p4": { "qed": { "total": 1,
                                                       "valid": 1 },
                                              "wp:main": { "total": 1,
                                                           "valid": 1 } },
                            "f_ensures_p3": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p2": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p1": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "f_ensures_p0": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 0 } },
+                                                          "valid": 1 } },
                            "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 34,
-                                                                    "valid": 34,
-                                                                    "rank": 0 },
+                                                                    "valid": 34 },
                                            "qed": { "total": 8, "valid": 8 },
                                            "wp:main": { "total": 42,
-                                                        "valid": 42,
-                                                        "rank": 0 } } } } }
+                                                        "valid": 42 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
index 8a4506b88c4a87d8e13a03c7e04048e9fa5b3b67..eb84ef54e1719a8eb9e9af4afa0e1caba90ad8f2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
@@ -53,5 +53,5 @@
 [wp] Report out: 'tests/wp_acsl/result_qualif/e_imply.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-f                    8     34 (1..8)        42       100%
+f                    8     34               42       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
index d6ca451c6b4efa8cb9f5c7ff5e33fa5744bc2c70..6fe581a3fda56826a0a36332c0216385690fe68c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
@@ -1,11 +1,9 @@
 { "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 2, "valid": 2, "rank": 0 },
                  "wp:main": { "total": 2, "valid": 2, "rank": 1 } },
   "wp:functions": { "foo": { "foo_assert_B": { "why3:Alt-Ergo,2.0.0": 
-                                                 { "total": 1, "valid": 1,
-                                                   "rank": 0 },
+                                                 { "total": 1, "valid": 1 },
                                                "wp:main": { "total": 1,
-                                                            "valid": 1,
-                                                            "rank": 1 } },
+                                                            "valid": 1 } },
                              "foo_assert_A": { "why3:Alt-Ergo,2.0.0": 
                                                  { "total": 1, "valid": 1,
                                                    "rank": 0 },
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
index 8de21842d8fbb97d1358643df647726d2fe518c2..aaee4540972d46c81da4020f16b346c55f521fd0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_acsl/tset.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 4 goals scheduled
 [wp] [Qed] Goal typed_lemma_UNION_DESCR : Valid
 [wp] [Alt-Ergo 2.0.0] Goal typed_lemma_UNION_EQ : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/tset.i b/src/plugins/wp/tests/wp_acsl/tset.i
index f55445cd7fade2d9cb14d57a585e303f49cfdd40..1a8d3616255affc8528b54ed60eeffdfcdb259e3 100644
--- a/src/plugins/wp/tests/wp_acsl/tset.i
+++ b/src/plugins/wp/tests/wp_acsl/tset.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-   OPT: -wp -wp-prover alt-ergo,coq -wp-coq-script tests/wp_acsl/tset.s
+   OPT: -wp -wp-prover alt-ergo,native:coq -wp-coq-script tests/wp_acsl/tset.s
 */
 
 /*@
diff --git a/src/plugins/wp/tests/wp_bts/bts_1174.i b/src/plugins/wp/tests/wp_bts/bts_1174.i
index fbc70fef492d18c3647cd8a9f19a7d0cd35bf985..da0bbc53889ea3e922863c157fefba16f2561866 100644
--- a/src/plugins/wp/tests/wp_bts/bts_1174.i
+++ b/src/plugins/wp/tests/wp_bts/bts_1174.i
@@ -1,5 +1,5 @@
 /* run.config_qualif
-   OPT: -wp -wp-prover coq -wp-coq-script tests/wp_bts/bts_1174.s -wp-model +real
+   OPT: -wp -wp-prover native:coq -wp-coq-script tests/wp_bts/bts_1174.s -wp-model +real
 */
 
 /*@ requires -10. <= x && x <= 10.; */
diff --git a/src/plugins/wp/tests/wp_bts/issue_143.i b/src/plugins/wp/tests/wp_bts/issue_143.i
index bf8b0ff6e1bf9d22f34b168c7e0f4a43cb96b0be..555cbcb5b0889741e7ebe50de2d0713662fb9934 100644
--- a/src/plugins/wp/tests/wp_bts/issue_143.i
+++ b/src/plugins/wp/tests/wp_bts/issue_143.i
@@ -4,9 +4,9 @@
 /* run.config_qualif
    EXECNOW: chmod a-x ./tests/inexistant-prover
    OPT: -wp
-   OPT: -wp -wp-prover "alt-ergo,coq" -wp-alt-ergo ./tests/inexistant-prover -wp-coqc ./tests/inexistant-prover
+   OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo ./tests/inexistant-prover -wp-coqc ./tests/inexistant-prover
    OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo ./tests/inexistant-prover
-   OPT: -wp -wp-prover "coq" -wp-coqc ./tests/inexistant-prover
+   OPT: -wp -wp-prover "native:coq" -wp-coqc ./tests/inexistant-prover
 */
  
 /*@
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 54d45f3925f1f9d511f7d0f85546683e15f2b689..632e1429bf1e00f533f2f72cb0d829a8f6d00211 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -96,16 +96,16 @@ end
     
     (* use frama_c_wp.memory.Memory *)
     
-    (* use S2_A *)
-    
     (* use Compound *)
     
     goal wp_goal :
-      forall t:addr -> int, t1:addr -> int, a:addr, a1:addr.
-       let a2 = Load_S2_A a t in
-       let a3 = Load_S2_A a (havoc t1 t a 1) in
+      forall t:int -> int, t1:addr -> int, a:addr, a1:addr, i:int.
+       let a2 = shiftfield_F1_FD_pos a1 in
+       let x = get t1 a2 in
+       not x = i ->
        region (base a1) <= 0 ->
-       region (base a) <= 0 -> IsS2_A a2 -> IsS2_A a3 -> EqS2_A a3 a2
+       region (base a) <= 0 ->
+       linked t -> is_sint32 i -> is_sint32 x -> not invalid t a2 1 -> a2 = a
   end
 [wp:print-generated] 
   theory WP1
@@ -125,15 +125,15 @@ end
     
     (* use frama_c_wp.memory.Memory *)
     
+    (* use S2_A *)
+    
     (* use Compound *)
     
     goal wp_goal :
-      forall t:int -> int, t1:addr -> int, a:addr, a1:addr, i:int.
-       let a2 = shiftfield_F1_FD_pos a1 in
-       let x = get t1 a2 in
-       not x = i ->
+      forall t:addr -> int, t1:addr -> int, a:addr, a1:addr.
+       let a2 = Load_S2_A a t in
+       let a3 = Load_S2_A a (havoc t1 t a 1) in
        region (base a1) <= 0 ->
-       region (base a) <= 0 ->
-       linked t -> is_sint32 i -> is_sint32 x -> not invalid t a2 1 -> a2 = a
+       region (base a) <= 0 -> IsS2_A a2 -> IsS2_A a3 -> EqS2_A a3 a2
   end
 [wp] 2 goals generated
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index 6ade8dc8e47d7d62db7bc92fceb4ac95519e0ca2..d896e322fd3320bd1a0aaa355b0dd971e9b9eb6c 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -16,5 +16,5 @@
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
 f3                   1     -                 1       100%
-g3                   1      2 (1..12)        3       100%
+g3                   1      2                3       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
index 4de546639bdce94817bb66c119bd9dd11ea8bb1e..9e6177b2266e249a4829326674529e789e00762d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
 [wp] [Coq] Goal typed_real_job_assert_qed_ok : Saved script
 [wp] [Coq (Native)] Goal typed_real_job_assert_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
index 68dc1319cde49b90405061a831cef2979123dab9..d1bac58fc498ae25867f0a51a83cbcea2f94f795 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.1.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
 [wp] [Alt-Ergo (Native)] Goal typed_foo_assert_ko : Unsuccess
 [wp] Proved goals:    0 / 1
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
index 6c44b75068c14cfa5ea543478657ca61008ceeef..c83a6e29b181ad4907472692dddfebddeafa80c3 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2471.2.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
 [wp] [Coq] Goal typed_foo_assert_ko : Default tactic
 [wp] [Coq (Native)] Goal typed_foo_assert_ko : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
index 6985b4d2e2f79547295f3d204986459fe4b042e5..3da99f6f4166562a7d709739d98a05aad12f7cf7 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo 2.0.0] Goal typed_lemma_ok_because_inconsistent : Valid
 [wp] [Alt-Ergo 2.0.0] Goal typed_lemma_ok_because_consistent : Valid
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
index e9bc0c7109c1f4fcb013f7f3a1586a9cbcedf86d..a9171eb8418720ec232899852ae3badcfbe5934d 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
 [wp] [Coq (Native)] Goal typed_lemma_ok_because_inconsistent : Failed
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
index ec62cdf34b1f7eef83897b5dd0f04f40c77fc8c2..32a7cab92e8f4145b8359eaa4952a7778af2db67 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
@@ -1,14 +1,10 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 0 },
-                 "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 },
+                 "wp:main": { "total": 1, "valid": 1 } },
   "wp:axiomatics": { "": { "lemma_foo": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                   "valid": 1,
-                                                                   "rank": 0 },
+                                                                   "valid": 1 },
                                           "wp:main": { "total": 1,
-                                                       "valid": 1,
-                                                       "rank": 1 } },
+                                                       "valid": 1 } },
                            "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                            "wp:main": { "total": 1,
-                                                        "valid": 1,
-                                                        "rank": 1 } } } } }
+                                                        "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
index f9611321b0c07ecc9cd0cd6a62b5fd80c99f8ad4..fe6b5998b58d94698d5b245fe644dbde90c64297 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
@@ -11,5 +11,5 @@
 [wp] Report out: 'tests/wp_bts/result_qualif/issue_447.0.report.json'
 -------------------------------------------------------------
 Axiomatics          WP     Alt-Ergo        Total   Success
-Lemma               -       1 (1..12)        1       100%
+Lemma               -       1                1       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/abs.i b/src/plugins/wp/tests/wp_plugin/abs.i
index 90f22cd6ab3a82191d3b1d88719576040cf71b59..1697ccefd8ee4b92eb75798d33d238f27df347aa 100644
--- a/src/plugins/wp/tests/wp_plugin/abs.i
+++ b/src/plugins/wp/tests/wp_plugin/abs.i
@@ -4,8 +4,8 @@
 
 /* run.config_qualif
    OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover alt-ergo
-   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover coq -wp-coq-script tests/wp_plugin/abs.script
-   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover why3:alt-ergo
+   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover native:coq -wp-coq-script tests/wp_plugin/abs.script
+   OPT: -wp -wp-driver tests/wp_plugin/abs.driver -wp-prover native:alt-ergo
 */
 
 /*@ axiomatic Absolute { logic integer ABS(integer x) ; } */
diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i
index cfc82845e9214f86571a6e907f5322fa7b2cbb8b..cee1e6f724b18f850abf81ed2ca31b4f373a7236 100644
--- a/src/plugins/wp/tests/wp_plugin/float_format.i
+++ b/src/plugins/wp/tests/wp_plugin/float_format.i
@@ -1,7 +1,7 @@
 /* run.config_qualif
-   OPT: -wp-prover coq
-   OPT: -wp-prover alt-ergo -wp-steps 50
-   OPT: -wp-prover why3:alt-ergo -wp-timeout 1
+   OPT: -wp-prover native:coq
+   OPT: -wp-prover native:alt-ergo -wp-steps 50 -wp-timeout 1
+   OPT: -wp-prover alt-ergo -wp-steps 50 -wp-timeout 1
 */
 
 //@ ensures KO: \result == 0.2 + x ;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index b4e08f2f351ade114947266fc0b50e60efdaefef..e9c5272c0cdca9ab2197a3eedc111a93dd229da1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp:print-generated] 
   "WPOUT/typed/Compound.v"
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 324363205674edba699cb8e9bfe8af0293e73744..55375f62ab76c16dc9f864f4786444ed828128cb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -94,35 +94,6 @@ Prove: P_P(x).
 ------------------------------------------------------------
 [wp] Running WP plugin...
 [wp] 2 goals scheduled
-[wp:print-generated] 
-  theory WP1
-    (* use why3.BuiltIn.BuiltIn *)
-    
-    (* use bool.Bool *)
-    
-    (* use int.Int *)
-    
-    (* use int.ComputerDivision *)
-    
-    (* use real.RealInfix *)
-    
-    (* use frama_c_wp.qed.Qed *)
-    
-    (* use map.Map *)
-    
-    (* use frama_c_wp.memory.Memory *)
-    
-    (* use frama_c_wp.cint.Cint *)
-    
-    (* use Compound *)
-    
-    (* use Axiomatic *)
-    
-    goal wp_goal :
-      forall t:addr -> int, i:int, a:addr.
-       let x = get t (shift_sint32 a i) in
-       region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
-  end
 ---------------------------------------------
 --- Context 'typed_ref_f' Cluster 'Compound' 
 ---------------------------------------------
@@ -166,7 +137,7 @@ theory Axiomatic1
   predicate P_P1 int
 end
 [wp:print-generated] 
-  theory WP2
+  theory WP1
     (* use why3.BuiltIn.BuiltIn *)
     
     (* use bool.Bool1 *)
@@ -194,6 +165,35 @@ end
        let x = get1 t (shift_sint321 a i) in
        region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
   end
+[wp:print-generated] 
+  theory WP2
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use bool.Bool *)
+    
+    (* use int.Int *)
+    
+    (* use int.ComputerDivision *)
+    
+    (* use real.RealInfix *)
+    
+    (* use frama_c_wp.qed.Qed *)
+    
+    (* use map.Map *)
+    
+    (* use frama_c_wp.memory.Memory *)
+    
+    (* use frama_c_wp.cint.Cint *)
+    
+    (* use Compound *)
+    
+    (* use Axiomatic *)
+    
+    goal wp_goal :
+      forall t:addr -> int, i:int, a:addr.
+       let x = get t (shift_sint32 a i) in
+       region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+  end
 [wp] 2 goals generated
 ------------------------------------------------------------
   Function f
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
index 4b9063d0f178130732921868959b1cc8bf2afca3..4d17c667443aeaffe5e5e6ed506a28dbb99fc946 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
 [wp] [Coq] Goal typed_abs_abs_ensures : Saved script
 [wp] [Coq (Native)] Goal typed_abs_abs_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
index c56a75a74f2900e6ff2ab6b0b7f26d96cb053126..442cf7ef208a98c392c23e686d3c8f07724f6fb9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle
@@ -3,14 +3,15 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_abs_abs_ensures : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_abs_abs_ensures : Valid
 [wp] Proved goals:    1 / 1
-  Qed:               0 
-  Alt-Ergo 2.0.0:    1
+  Qed:             0 
+  Alt-Ergo:        1
 [wp] Report in:  'tests/wp_plugin/oracle_qualif/abs.2.report.json'
 [wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-abs                 -       1 (12..24)       1       100%
+abs                 -      -  (4..16)        1       100%
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index 3dd881b83a080a87062470970a66d63508976476..dc04687542bb7b0243f7755dd022bb93735c82f9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 2 goals scheduled
 [wp] [Alt-Ergo (Native)] Goal typed_lemma_ceil : Valid
 [wp] [Alt-Ergo (Native)] Goal typed_lemma_floor : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index 8f2da577ae2b91e982e22236096af9b0387f36cf..e31c6d175775cd0375962688d6dcbbc1d558970b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
@@ -6,6 +6,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 1 goal scheduled
 [wp] [Coq] Goal typed_output_ensures_KO : Default tactic
 [wp] [Coq (Native)] Goal typed_output_ensures_KO : Unsuccess
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index 9f87d54d4ed370a5490dfc6b41b9a0f9e81abe2d..d09e55d57ba5e9e07e15a0ba98da51ba018038cf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-steps 50 [...]
+# frama-c -wp -wp-timeout 1 -wp-steps 50 [...]
 [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
 [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: 
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
@@ -6,10 +6,11 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 1 goal scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_output_ensures_KO : Unsuccess
+[wp] [Alt-Ergo (Native)] Goal typed_output_ensures_KO : Unsuccess
 [wp] Proved goals:    0 / 1
-  Alt-Ergo 2.0.0:    0  (unsuccess: 1)
+  Alt-Ergo:        0  (unsuccess: 1)
 [wp] Report in:  'tests/wp_plugin/oracle_qualif/float_format.1.report.json'
 [wp] Report out: 'tests/wp_plugin/result_qualif/float_format.1.report.json'
 -------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index 2230d173868d3de4a87b2ea35b6a238d9a296e24..5bb10c8461a7fa2ca51ebca73decf4548deb6973 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 1 [...]
+# frama-c -wp -wp-timeout 1 -wp-steps 50 [...]
 [kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
 [kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning: 
   Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
index 58f1a2f1d9209618e89faafebbc1c4254004245b..d63839a64a15552a8592daa867693750a73a4b56 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle
@@ -2,6 +2,7 @@
 [kernel] Parsing tests/wp_plugin/inductive.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
+[wp] Warning: native support for coq is deprecated, use tip instead
 [wp] 2 goals scheduled
 [wp] [Coq] Goal typed_lemma_offset : Saved script
 [wp] [Coq] Goal typed_lemma_offset : Default tactic
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
index 902a09e4e83ab6fb2d5bc6cb54f3bb2a1659e873..1f29e24d9a523b995f3eace64198f8f3043ce299 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.1.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 30 goals scheduled
 [wp] [Alt-Ergo (Native)] Goal typed_lemma_abs_neg : Valid
 [wp] [Alt-Ergo (Native)] Goal typed_lemma_abs_pos : Valid
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index 6117c36a1ed9e8201c05943529493aeac4879fa4..4f28996c39a4372709586db9f90b6bed6b6c78f5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -3,6 +3,7 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+[wp] Warning: native support for alt-ergo is deprecated, use why3 instead
 [wp] 9 goals scheduled
 [wp] [Alt-Ergo (Native)] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
 [wp] [Alt-Ergo (Native)] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
index 5d34a2aa148ec69a768c4de87205861440f6366d..174835a1aa1206e5e4fb046badfcc607c4caf659 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.0.report.json
@@ -1,14 +1,10 @@
-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 1 },
-                 "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 },
+                 "wp:main": { "total": 1, "valid": 1 } },
   "wp:functions": { "Job": { "Job_ensures": { "why3:Alt-Ergo,2.0.0": 
-                                                { "total": 1, "valid": 1,
-                                                  "rank": 1 },
+                                                { "total": 1, "valid": 1 },
                                               "wp:main": { "total": 1,
-                                                           "valid": 1,
-                                                           "rank": 1 } },
+                                                           "valid": 1 } },
                              "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 1 },
+                                                                    "valid": 1 },
                                              "wp:main": { "total": 1,
-                                                          "valid": 1,
-                                                          "rank": 1 } } } } }
+                                                          "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 48f19a88154aac3ef6ba18614891f4c87c71fdaa..487049986e2a19d8714a9bad06ff32efabe7b552 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -14,5 +14,5 @@
 [wp] Report out: 'tests/wp_typed/result_qualif/mvar.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-Job                 -       1 (1..12)        1       100%
+Job                 -       1                1       100%
 -------------------------------------------------------------