diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index f6e58803126e64ca589f206486ac83566185012d..24527f5f773630af9474ca1b0953746e467a7a0f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -347,8 +347,8 @@ struct
     List.fold_right (use_property env) bhv.bhv_assumes @@
     List.fold_right (use_property env) bhv.bhv_requires @@
     List.fold_right (use_property env) (behaviors kf) @@
-    List.fold_right (use_property env) (complete mode kf) @@
-    List.fold_right (use_property env) (disjoint mode kf) @@
+    List.fold_right (prove_property env) (complete mode kf) @@
+    List.fold_right (prove_property env) (disjoint mode kf) @@
     (* frame-in *)
     W.scope env.we xs SC_Frame_in @@
     (* function body *)