diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index dec7620bbed146fcf63f176ff221d19eec7d3f54..272f255fe7f5bdc28c13f9f4fe29d538d217b6f9 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -565,13 +565,17 @@ module Cfg (W : Mcfg.S) = struct
       | Cil2cfg.VblkIn (Cil2cfg.Bfct, b) ->
           let obj = get_only_succ env cfg v in
           let obj = wp_scope wenv b.blocals Mcfg.SC_Block_in obj in
-          wp_scope wenv formals Mcfg.SC_Function_frame obj
+          let obj = wp_scope wenv formals Mcfg.SC_Function_frame obj in
+          obj
+      | Cil2cfg.VblkOut (Cil2cfg.Bfct, b) ->
+          let obj = get_only_succ env cfg v in
+          let obj = wp_scope wenv b.blocals Mcfg.SC_Block_out obj in
+          obj
+      | Cil2cfg.VblkOut _ ->
+          get_only_succ env cfg v
       | Cil2cfg.VblkIn (_, b) ->
           let obj = get_only_succ env cfg v in
           wp_scope wenv b.blocals Mcfg.SC_Block_in obj
-      | Cil2cfg.VblkOut (_, _b) ->
-          let obj = get_only_succ env cfg v in
-          obj (* cf. blocks_closed_by_edge below *)
       | Cil2cfg.Vstmt s ->
           let obj = get_only_succ env cfg v in
           wp_stmt wenv s obj