diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 01e99eacd7fea4a704a07da3306054e24710e543..dec7620bbed146fcf63f176ff221d19eec7d3f54 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -494,8 +494,9 @@ module Cfg (W : Mcfg.S) = struct
        | Mcfg.SC_Function_frame -> "function frame"
        | Mcfg.SC_Function_out -> "function out" )
       (Pretty_utils.pp_list  ~sep:", " Printer.pp_varinfo) vars;
-    W.scope wenv vars scope obj
-
+    match scope with
+    | Mcfg.(SC_Block_in | SC_Block_out) when vars = [] -> obj
+    | _ -> W.scope wenv vars scope obj
 
   (** @return the WP stored for edge [e]. Compute it if it is not already
    * there and store it. Also handle the Acut annotations. *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot
index 9b4f1de3952bd66b028d1df4dd8ce7f4c147085a..077cfed3a2e1434664df16c14606fadf8d9e4e0c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f.dot
@@ -2,89 +2,73 @@ digraph f {
   rankdir = TB ;
   node [ style = filled, shape = box ] ;
   N000 [ color = red, shape = circle, label = "*" ] ;
-  N074 [ color=red , label="Prove f_ensures" ] ;
-  N074 -> N000 [ style=dotted ] ;
-  N075 [ color=red , label="Prove f_ensures_2" ] ;
-  N075 -> N074 [ style=dotted ] ;
-  N076 [ label="" , shape=circle ] ;
+  N056 [ color=red , label="Prove f_ensures" ] ;
+  N056 -> N000 [ style=dotted ] ;
+  N057 [ color=red , label="Prove f_ensures_2" ] ;
+  N057 -> N056 [ style=dotted ] ;
+  N058 [ label="" , shape=circle ] ;
+ N058 -> N057 ;
+ N058 -> N056 ;
+  N059 [ color=lightblue , label="F-out { a b }" ] ;
+ N059 -> N058 ;
+  N060 [ label="Label wp:post" ] ;
+ N060 -> N059 ;
+  N061 [ color=lightblue , label="B-out { __retres }" ] ;
+ N061 -> N060 ;
+  N062 [ color=orange , label="Return __retres" ] ;
+ N062 -> N061 ;
+  N063 [ label="Label wp:sid27 (Stmt s27)" ] ;
+ N063 -> N062 ;
+  N064 [ label="Label wp:sid26 (Stmt s26)" ] ;
+ N064 -> N063 ;
+  N065 [ color=green , label="Assume f_assert" ] ;
+ N065 -> N064 ;
+  N066 [ color=red , label="Prove f_assert" ] ;
+  N066 -> N065 [ style=dotted ] ;
+  N067 [ label="" , shape=circle ] ;
+ N067 -> N066 ;
+ N067 -> N065 ;
+  N068 [ label="Label wp:sid25 (Stmt s25)" ] ;
+ N068 -> N067 ;
+  N069 [ color=orange , label="__retres := a + b" ] ;
+ N069 -> N068 ;
+  N070 [ label="Label wp:sid6 (Stmt s6)" ] ;
+ N070 -> N069 ;
+  N071 [ label="Label wp:sid24 (Stmt s24)" ] ;
+ N071 -> N070 ;
+  N072 [ color=orange , label="Return __retres" ] ;
+ N072 -> N061 ;
+  N073 [ label="Label wp:sid27 (Stmt s27)" ] ;
+ N073 -> N072 ;
+  N074 [ color=orange , label="__retres := -1" ] ;
+ N074 -> N073 ;
+  N075 [ label="Label wp:sid8 (Stmt s8)" ] ;
+ N075 -> N074 ;
+  N076 [ color=green , label="Assume f_ensures_3" ] ;
  N076 -> N075 ;
- N076 -> N074 ;
-  N077 [ color=lightblue , label="F-out { a b }" ] ;
+  N077 [ color=orange , label="Havoc f_assigns:
+assigns __retres;" ] ;
  N077 -> N076 ;
-  N078 [ label="Label wp:post" ] ;
- N078 -> N077 ;
-  N079 [ color=lightblue , label="B-out { __retres }" ] ;
+  N078 [ color=cyan , label="If a > 0" ] ;
+ N078 -> N071 ;
+ N078 -> N000 [ style=dotted ];
+  N079 [ label="Label wp:sid4 (Stmt s4)" ] ;
  N079 -> N078 ;
-  N080 [ color=orange , label="Return __retres" ] ;
+  N080 [ label="" , shape=circle ] ;
+ N080 -> N077 ;
  N080 -> N079 ;
-  N081 [ color=lightblue , label="B-out { }" ] ;
+  N081 [ label="Label wp:sid2 (Stmt s2)" ] ;
  N081 -> N080 ;
-  N082 [ color=lightblue , label="B-out { }" ] ;
+  N082 [ color=lightblue , label="B-in { __retres }" ] ;
  N082 -> N081 ;
-  N083 [ color=lightblue , label="B-out { }" ] ;
+  N083 [ color=lightblue , label="F-frame { a b }" ] ;
  N083 -> N082 ;
-  N084 [ label="Label wp:sid27 (Stmt s27)" ] ;
+  N084 [ label="Label wp:pre" ] ;
  N084 -> N083 ;
-  N085 [ label="Label wp:sid26 (Stmt s26)" ] ;
+  N085 [ color=lightblue , label="F-in { a b }" ] ;
  N085 -> N084 ;
-  N086 [ color=green , label="Assume f_assert" ] ;
+  N086 [ color=lightblue , label="Global { }" ] ;
  N086 -> N085 ;
-  N087 [ color=red , label="Prove f_assert" ] ;
-  N087 -> N086 [ style=dotted ] ;
-  N088 [ label="" , shape=circle ] ;
- N088 -> N087 ;
- N088 -> N086 ;
-  N089 [ label="Label wp:sid25 (Stmt s25)" ] ;
- N089 -> N088 ;
-  N090 [ color=orange , label="__retres := a + b" ] ;
- N090 -> N089 ;
-  N091 [ label="Label wp:sid6 (Stmt s6)" ] ;
- N091 -> N090 ;
-  N092 [ color=lightblue , label="B-in { }" ] ;
- N092 -> N091 ;
-  N093 [ label="Label wp:sid24 (Stmt s24)" ] ;
- N093 -> N092 ;
-  N094 [ color=lightblue , label="B-in { }" ] ;
- N094 -> N093 ;
-  N095 [ color=orange , label="Return __retres" ] ;
- N095 -> N079 ;
-  N096 [ label="Label wp:sid27 (Stmt s27)" ] ;
- N096 -> N095 ;
-  N097 [ color=orange , label="__retres := -1" ] ;
- N097 -> N096 ;
-  N098 [ label="Label wp:sid8 (Stmt s8)" ] ;
- N098 -> N097 ;
-  N099 [ color=green , label="Assume f_ensures_3" ] ;
- N099 -> N098 ;
-  N100 [ color=orange , label="Havoc f_assigns:
-assigns __retres;" ] ;
- N100 -> N099 ;
-  N101 [ color=lightblue , label="B-in { }" ] ;
- N101 -> N000 [ style=dotted ];
-  N102 [ color=lightblue , label="B-out { }" ] ;
- N102 -> N101 ;
-  N103 [ color=cyan , label="If a > 0" ] ;
- N103 -> N094 ;
- N103 -> N102 ;
-  N104 [ label="Label wp:sid4 (Stmt s4)" ] ;
- N104 -> N103 ;
-  N105 [ color=lightblue , label="B-in { }" ] ;
- N105 -> N104 ;
-  N106 [ label="" , shape=circle ] ;
- N106 -> N100 ;
- N106 -> N105 ;
-  N107 [ label="Label wp:sid2 (Stmt s2)" ] ;
- N107 -> N106 ;
-  N108 [ color=lightblue , label="B-in { __retres }" ] ;
- N108 -> N107 ;
-  N109 [ color=lightblue , label="F-frame { a b }" ] ;
- N109 -> N108 ;
-  N110 [ label="Label wp:pre" ] ;
- N110 -> N109 ;
-  N111 [ color=lightblue , label="F-in { a b }" ] ;
- N111 -> N110 ;
-  N112 [ color=lightblue , label="Global { }" ] ;
- N112 -> N111 ;
-  N113 [ color=cyan , label="Function f" ] ;
- N113 -> N112 ;
+  N087 [ color=cyan , label="Function f" ] ;
+ N087 -> N086 ;
 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
index e5347d619f1af81ecddd15d1235eea49dbb1e2b1..be3a8a3a5db7557308b6a855e36ed03b49a2a6ea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/f_default_for_stmt_2.dot
@@ -2,80 +2,64 @@ digraph f {
   rankdir = TB ;
   node [ style = filled, shape = box ] ;
   N000 [ color = red, shape = circle, label = "*" ] ;
-  N114 [ color=lightblue , label="F-out { a b }" ] ;
- N114 -> N000 [ style=dotted ];
-  N115 [ label="Label wp:post" ] ;
+  N088 [ color=lightblue , label="F-out { a b }" ] ;
+ N088 -> N000 [ style=dotted ];
+  N089 [ label="Label wp:post" ] ;
+ N089 -> N088 ;
+  N090 [ color=lightblue , label="B-out { __retres }" ] ;
+ N090 -> N089 ;
+  N091 [ color=orange , label="Return __retres" ] ;
+ N091 -> N090 ;
+  N092 [ label="Label wp:sid27 (Stmt s27)" ] ;
+ N092 -> N091 ;
+  N093 [ label="Label wp:sid26 (Stmt s26)" ] ;
+ N093 -> N092 ;
+  N094 [ color=green , label="Assume f_assert" ] ;
+ N094 -> N093 ;
+  N095 [ label="Label wp:sid25 (Stmt s25)" ] ;
+ N095 -> N094 ;
+  N096 [ color=orange , label="__retres := a + b" ] ;
+ N096 -> N095 ;
+  N097 [ label="Label wp:sid6 (Stmt s6)" ] ;
+ N097 -> N096 ;
+  N098 [ label="Label wp:sid24 (Stmt s24)" ] ;
+ N098 -> N097 ;
+  N099 [ color=orange , label="Return __retres" ] ;
+ N099 -> N090 ;
+  N100 [ label="Label wp:sid27 (Stmt s27)" ] ;
+ N100 -> N099 ;
+  N101 [ color=orange , label="__retres := -1" ] ;
+ N101 -> N100 ;
+  N102 [ label="Label wp:sid8 (Stmt s8)" ] ;
+ N102 -> N101 ;
+  N103 [ color=green , label="Assume f_ensures_3" ] ;
+ N103 -> N102 ;
+  N104 [ color=red , label="Assigns f_assigns" ] ;
+  N105 [ label="" , shape=circle ] ;
+ N105 -> N104 ;
+ N105 -> N103 ;
+  N106 [ color=red , label="Prove f_ensures_3" ] ;
+  N106 -> N105 [ style=dotted ] ;
+  N107 [ label="" , shape=circle ] ;
+ N107 -> N106 ;
+ N107 -> N105 ;
+  N108 [ color=cyan , label="If a > 0" ] ;
+ N108 -> N098 ;
+ N108 -> N107 ;
+  N109 [ label="Label wp:sid4 (Stmt s4)" ] ;
+ N109 -> N108 ;
+  N110 [ label="Label wp:sid2 (Stmt s2)" ] ;
+ N110 -> N109 ;
+  N111 [ color=lightblue , label="B-in { __retres }" ] ;
+ N111 -> N110 ;
+  N112 [ color=lightblue , label="F-frame { a b }" ] ;
+ N112 -> N111 ;
+  N113 [ label="Label wp:pre" ] ;
+ N113 -> N112 ;
+  N114 [ color=lightblue , label="F-in { a b }" ] ;
+ N114 -> N113 ;
+  N115 [ color=lightblue , label="Global { }" ] ;
  N115 -> N114 ;
-  N116 [ color=lightblue , label="B-out { __retres }" ] ;
+  N116 [ color=cyan , label="Function f" ] ;
  N116 -> N115 ;
-  N117 [ color=orange , label="Return __retres" ] ;
- N117 -> N116 ;
-  N118 [ color=lightblue , label="B-out { }" ] ;
- N118 -> N117 ;
-  N119 [ color=lightblue , label="B-out { }" ] ;
- N119 -> N118 ;
-  N120 [ color=lightblue , label="B-out { }" ] ;
- N120 -> N119 ;
-  N121 [ label="Label wp:sid27 (Stmt s27)" ] ;
- N121 -> N120 ;
-  N122 [ label="Label wp:sid26 (Stmt s26)" ] ;
- N122 -> N121 ;
-  N123 [ color=green , label="Assume f_assert" ] ;
- N123 -> N122 ;
-  N124 [ label="Label wp:sid25 (Stmt s25)" ] ;
- N124 -> N123 ;
-  N125 [ color=orange , label="__retres := a + b" ] ;
- N125 -> N124 ;
-  N126 [ label="Label wp:sid6 (Stmt s6)" ] ;
- N126 -> N125 ;
-  N127 [ color=lightblue , label="B-in { }" ] ;
- N127 -> N126 ;
-  N128 [ label="Label wp:sid24 (Stmt s24)" ] ;
- N128 -> N127 ;
-  N129 [ color=lightblue , label="B-in { }" ] ;
- N129 -> N128 ;
-  N130 [ color=orange , label="Return __retres" ] ;
- N130 -> N116 ;
-  N131 [ label="Label wp:sid27 (Stmt s27)" ] ;
- N131 -> N130 ;
-  N132 [ color=orange , label="__retres := -1" ] ;
- N132 -> N131 ;
-  N133 [ label="Label wp:sid8 (Stmt s8)" ] ;
- N133 -> N132 ;
-  N134 [ color=green , label="Assume f_ensures_3" ] ;
- N134 -> N133 ;
-  N135 [ color=red , label="Assigns f_assigns" ] ;
-  N136 [ label="" , shape=circle ] ;
- N136 -> N135 ;
- N136 -> N134 ;
-  N137 [ color=red , label="Prove f_ensures_3" ] ;
-  N137 -> N136 [ style=dotted ] ;
-  N138 [ label="" , shape=circle ] ;
- N138 -> N137 ;
- N138 -> N136 ;
-  N139 [ color=lightblue , label="B-in { }" ] ;
- N139 -> N138 ;
-  N140 [ color=lightblue , label="B-out { }" ] ;
- N140 -> N139 ;
-  N141 [ color=cyan , label="If a > 0" ] ;
- N141 -> N129 ;
- N141 -> N140 ;
-  N142 [ label="Label wp:sid4 (Stmt s4)" ] ;
- N142 -> N141 ;
-  N143 [ color=lightblue , label="B-in { }" ] ;
- N143 -> N142 ;
-  N144 [ label="Label wp:sid2 (Stmt s2)" ] ;
- N144 -> N143 ;
-  N145 [ color=lightblue , label="B-in { __retres }" ] ;
- N145 -> N144 ;
-  N146 [ color=lightblue , label="F-frame { a b }" ] ;
- N146 -> N145 ;
-  N147 [ label="Label wp:pre" ] ;
- N147 -> N146 ;
-  N148 [ color=lightblue , label="F-in { a b }" ] ;
- N148 -> N147 ;
-  N149 [ color=lightblue , label="Global { }" ] ;
- N149 -> N148 ;
-  N150 [ color=cyan , label="Function f" ] ;
- N150 -> N149 ;
 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot b/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot
index 5cdbeab832713294f78f544c2edaf44cee84135c..4fffdb8fb16edd8f2e3eb57b430c493b7f3da9f4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/g.dot
@@ -2,55 +2,47 @@ digraph g {
   rankdir = TB ;
   node [ style = filled, shape = box ] ;
   N000 [ color = red, shape = circle, label = "*" ] ;
-  N049 [ color=red , label="Prove g_ensures_2" ] ;
-  N049 -> N000 [ style=dotted ] ;
-  N050 [ color=lightblue , label="F-out { a b }" ] ;
+  N035 [ color=red , label="Prove g_ensures_2" ] ;
+  N035 -> N000 [ style=dotted ] ;
+  N036 [ color=lightblue , label="F-out { a b }" ] ;
+ N036 -> N035 ;
+  N037 [ label="Label wp:post" ] ;
+ N037 -> N036 ;
+  N038 [ color=lightblue , label="B-out { __retres }" ] ;
+ N038 -> N037 ;
+  N039 [ color=orange , label="Return __retres" ] ;
+ N039 -> N038 ;
+  N040 [ label="Label wp:sid32 (Stmt s32)" ] ;
+ N040 -> N039 ;
+  N041 [ label="Label wp:sid31 (Stmt s31)" ] ;
+ N041 -> N040 ;
+  N042 [ color=green , label="Assume g_assert" ] ;
+ N042 -> N041 ;
+  N043 [ color=red , label="Prove g_assert" ] ;
+  N043 -> N042 [ style=dotted ] ;
+  N044 [ label="" , shape=circle ] ;
+ N044 -> N043 ;
+ N044 -> N042 ;
+  N045 [ label="Label wp:sid30 (Stmt s30)" ] ;
+ N045 -> N044 ;
+  N046 [ color=orange , label="__retres := a + b" ] ;
+ N046 -> N045 ;
+  N047 [ label="Label wp:sid13 (Stmt s13)" ] ;
+ N047 -> N046 ;
+  N048 [ label="Label wp:sid29 (Stmt s29)" ] ;
+ N048 -> N047 ;
+  N049 [ label="Label wp:sid11 (Stmt s11)" ] ;
+ N049 -> N048 ;
+  N050 [ color=lightblue , label="B-in { __retres }" ] ;
  N050 -> N049 ;
-  N051 [ label="Label wp:post" ] ;
+  N051 [ color=lightblue , label="F-frame { a b }" ] ;
  N051 -> N050 ;
-  N052 [ color=lightblue , label="B-out { __retres }" ] ;
+  N052 [ label="Label wp:pre" ] ;
  N052 -> N051 ;
-  N053 [ color=orange , label="Return __retres" ] ;
+  N053 [ color=lightblue , label="F-in { a b }" ] ;
  N053 -> N052 ;
-  N054 [ color=lightblue , label="B-out { }" ] ;
+  N054 [ color=lightblue , label="Global { }" ] ;
  N054 -> N053 ;
-  N055 [ color=lightblue , label="B-out { }" ] ;
+  N055 [ color=cyan , label="Function g" ] ;
  N055 -> N054 ;
-  N056 [ label="Label wp:sid32 (Stmt s32)" ] ;
- N056 -> N055 ;
-  N057 [ label="Label wp:sid31 (Stmt s31)" ] ;
- N057 -> N056 ;
-  N058 [ color=green , label="Assume g_assert" ] ;
- N058 -> N057 ;
-  N059 [ color=red , label="Prove g_assert" ] ;
-  N059 -> N058 [ style=dotted ] ;
-  N060 [ label="" , shape=circle ] ;
- N060 -> N059 ;
- N060 -> N058 ;
-  N061 [ label="Label wp:sid30 (Stmt s30)" ] ;
- N061 -> N060 ;
-  N062 [ color=orange , label="__retres := a + b" ] ;
- N062 -> N061 ;
-  N063 [ label="Label wp:sid13 (Stmt s13)" ] ;
- N063 -> N062 ;
-  N064 [ color=lightblue , label="B-in { }" ] ;
- N064 -> N063 ;
-  N065 [ label="Label wp:sid29 (Stmt s29)" ] ;
- N065 -> N064 ;
-  N066 [ color=lightblue , label="B-in { }" ] ;
- N066 -> N065 ;
-  N067 [ label="Label wp:sid11 (Stmt s11)" ] ;
- N067 -> N066 ;
-  N068 [ color=lightblue , label="B-in { __retres }" ] ;
- N068 -> N067 ;
-  N069 [ color=lightblue , label="F-frame { a b }" ] ;
- N069 -> N068 ;
-  N070 [ label="Label wp:pre" ] ;
- N070 -> N069 ;
-  N071 [ color=lightblue , label="F-in { a b }" ] ;
- N071 -> N070 ;
-  N072 [ color=lightblue , label="Global { }" ] ;
- N072 -> N071 ;
-  N073 [ color=cyan , label="Function g" ] ;
- N073 -> N072 ;
 }