diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 272f255fe7f5bdc28c13f9f4fe29d538d217b6f9..2f3c5e7e07f6e2642da5d4073d8e85e545bfee84 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -571,11 +571,8 @@ module Cfg (W : Mcfg.S) = struct
           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 _ ->
+      | Cil2cfg.VblkOut _ | Cil2cfg.VblkIn _ ->
           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.Vstmt s ->
           let obj = get_only_succ env cfg v in
           wp_stmt wenv s obj
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 8a8402eb8712585dad6ecd71d56850b4a54d0202..0afef00829bce0f5af4c9d58aedf3ddf44de2861 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -653,7 +653,11 @@ let block_scope_for_edge cfg e =
             | None -> no_scope
             | Some s' -> block_scope s s'
       end
-  | _ -> (* TODO ? *) no_scope
+  | VblkIn(Bstmt _,b) -> { b_opened=[b] ; b_closed=[] }
+  | Vcall _
+  | VblkIn _ | VblkOut _ | Vtest(false,_,_)
+  | VfctIn | VfctOut | Vstart | Vend | Vexit | Vloop2 _ ->
+      no_scope
 
 let has_exit cfg =
   try