diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 8c109303a4d6e40a5dbda7d51f0cad5ff73f8079..2276eb131fdf5f62e24b164dcabc74386e1fc51a 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -187,6 +187,8 @@ struct
            WpContext.on_context (model,WpContext.Kf mode.kf)
              begin fun () ->
                LogicUsage.iter_lemmas VCG.register_lemma ;
+               if WpRTE.missing_guards model mode.kf then
+                 warning ~current:false ~once:true "Missing RTE guards" ;
                let bhv =
                  if Cil.is_default_behavior mode.bhv then None
                  else Some mode.bhv.b_name in