diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 1142f94be4a6a2332587601bed23facc45797380..be0a373cd906495eb6be696eb664c0fa967b3943 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -231,6 +231,7 @@ struct
     match edge.edge_transition with
     | Skip -> p
     | Return(r,s) -> W.return env.we s r p
+    | Enter { blocals=[] } | Leave { blocals=[] } -> p
     | Enter { blocals=xs } -> W.scope env.we xs SC_Block_in p
     | Leave { blocals=xs } -> W.scope env.we xs SC_Block_out p
     | Instr (i,s) -> instr env s i p