diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 5ff18776daee314d628fd08a9b63d69f38bd916e..77b150a71b9f743f29deea6685f04b88d0fd128c 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -363,6 +363,11 @@ struct
     let req = default_requires mode kf in
     let bhv = CfgAnnot.get_behavior kf Kglobal has_exit ~active:[] mode.bhv in
 
+    let prove_if_main env ps =
+      if not @@ WpStrategy.is_main_init kf then Extlib.id
+      else List.fold_right (prove_property env) ps
+    in
+
     env.we ,
     (* global init *)
     W.close env.we @@
@@ -372,6 +377,7 @@ struct
     W.label env.we None Clabels.pre @@
     List.fold_right (use_property env) req @@
     List.fold_right (use_property env) bhv.bhv_assumes @@
+    prove_if_main env bhv.bhv_requires @@
     List.fold_right (use_property env) bhv.bhv_requires @@
     List.fold_right (use_property env) (behaviors kf) @@
     List.fold_right (prove_property env) (complete mode kf) @@