diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index a631bda083e13fe192f676a56c766e73930fcfa6..8e026f7bf045b539009a3bbeaf6b95316bb3ca55 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -748,8 +748,11 @@ let cmdline_run () =
     if fct <> Wp_parameters.Fct_none then
       begin
         Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
+        let computer = computer () in
         Ast.compute ();
         Dyncall.compute ();
+        if Wp_parameters.RTE.get () then
+          WpRTE.generate_all computer#model ;
         if Wp_parameters.has_dkey dkey_logicusage then
           begin
             LogicUsage.compute ();
@@ -763,7 +766,6 @@ let cmdline_run () =
         let bhv = Wp_parameters.Behaviors.get () in
         let prop = Wp_parameters.Properties.get () in
         (** TODO entry point *)
-        let computer = computer () in
         if Wp_parameters.has_dkey dkey_builtins then
           begin
             WpContext.on_context (computer#model,WpContext.Global)
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 74e6fdd198f0571fc00914d254d51eacbe7e330e..a6bc0690c67b02c398b4a689d52472dda12c11fb 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -102,6 +102,9 @@ let generate model kf =
   List.iter (configure ~update ~generate:true kf cint) generator ;
   if !update then !Db.RteGen.annotate_kf kf
 
+let generate_all model =
+  Wp_parameters.iter_kf (generate model)
+
 let missing_guards model kf =
   let update = ref false in
   let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
diff --git a/src/plugins/wp/wpRTE.mli b/src/plugins/wp/wpRTE.mli
index 53b0fc8eb4bedfaa029cf571b2a7bb01f75ea752..86ce77c668afd0e0d5c608baa35653d5e0b6c809 100644
--- a/src/plugins/wp/wpRTE.mli
+++ b/src/plugins/wp/wpRTE.mli
@@ -24,6 +24,9 @@
     for the given function and model. *)
 val generate : WpContext.model -> Kernel_function.t -> unit
 
+(** Invoke RTE on all selected functions *)
+val generate_all : WpContext.model -> unit
+
 (** Returns [true] if RTE annotations should be generated for
     the given function and model (and are not generated yet). *)
 val missing_guards : WpContext.model -> Kernel_function.t -> bool