diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index d886bdacd26e6ed444a456a45810ae25a261c159..fd907f9e54c4ab63c1badd4c5b879c3a8d713c9b 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -342,15 +342,16 @@ struct
     let requires_init = if init then b.bhv_requires else [] in
     (* pre-state *)
     W.label env.we None Clabels.pre @@
-    (* frame-in *)
-    W.scope env.we formals SC_Frame_in @@
     (* pre-conditions *)
     List.fold_right (use_property env) (default_requires env.mode kf) @@
     List.fold_right (use_property env) b.bhv_assumes @@
     List.fold_right (prove_property env) requires_init @@
     List.fold_right (use_property env) b.bhv_requires @@
     List.fold_right (prove_property env) b.bhv_smokes @@
-    List.fold_right (use_property env) side_behaviors w
+    List.fold_right (use_property env) side_behaviors @@
+    (* frame-in *)
+    W.scope env.we formals SC_Frame_in w
+
 
   let do_post env ~formals (b : CfgAnnot.behavior) w =
     W.scope env.we formals SC_Frame_out @@