diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 1ff49f9195b739542bc8dd696a200dcc43d16cba..01e99eacd7fea4a704a07da3306054e24710e543 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -605,11 +605,10 @@ module Cfg (W : Mcfg.S) = struct
                     wp_scope wenv formals Mcfg.SC_Function_after_POST obj
           *)
     in
-    let res =
-      let blks = Cil2cfg.blocks_closed_by_edge cfg e in
-      let free_locals res b = wp_scope wenv b.blocals Mcfg.SC_Block_out res in
-      List.fold_left free_locals res blks
-    in
+    let Cil2cfg.{ b_closed ; b_opened } = Cil2cfg.block_scope_for_edge cfg e in
+    let do_block sc res b = wp_scope wenv b.blocals sc res in
+    let res = List.fold_left (do_block Mcfg.SC_Block_in) res b_opened in
+    let res = List.fold_left (do_block Mcfg.SC_Block_out) res b_closed in
     debug "[compute_edge] before %a done@." Cil2cfg.pp_node v;
     Cil.CurrentLoc.set old_loc;
     res
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index b995b8212a44f2290f514d3b0d74e75509ff11b7..8a8402eb8712585dad6ecd71d56850b4a54d0202 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -626,36 +626,34 @@ let get_post_label cfg v =
       | None -> None
       | Some s -> Some (Clabels.stmt s)
 
-let blocks_closed_by_edge cfg e =
+type block_scope = { b_opened : block list ; b_closed : block list }
+
+let no_scope = { b_opened = [] ; b_closed = [] }
+
+let block_scope s s' =
+  try
+    {
+      b_opened = Kernel_function.blocks_opened_by_edge s s' ;
+      b_closed = Kernel_function.blocks_closed_by_edge s s' ;
+    }
+  with Not_found | Invalid_argument _ ->
+    debug "[blocks_closed_by_edge] not found sid:%d -> sid:%d@." s.sid s'.sid;
+    no_scope
+
+let block_scope_for_edge cfg e =
   debug "[blocks_closed_by_edge] for %a...@." pp_edge e;
   let v_before = edge_src e in
-  let blocks = match node_type v_before with
-    | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_) ->
-        ignore (Ast.get ()); (* Since CIL Cfg computation is required and
-                                                                Ast.get () have to do this well. *)
-        begin match s.succs with
-          | [s'] -> (try Kernel_function.blocks_closed_by_edge s s'
-                     with Not_found as e -> debug "[blocks_closed_by_edge] not found sid:%d -> sid:%d@."
-                                              s.sid s'.sid;
-                       raise e)
-          | [] | _ :: _ ->
-              let s' = get_edge_next_stmt cfg e in
-              match s' with
-              | None -> []
-              | Some s' ->
-                  debug
-                    "[blocks_closed_by_edge] found sid:%d -> sid:%d@."
-                    s.sid s'.sid;
-                  try Kernel_function.blocks_closed_by_edge s s'
-                  with Invalid_argument _ -> []
-        end
-    | _ -> (* TODO ? *) []
-  in
-  let v_after = edge_dst e in
-  let blocks = match node_type v_after with
-    | VblkOut (Bfct, b) -> b::blocks
-    | _ -> blocks
-  in blocks
+  match node_type v_before with
+  | Vstmt s | Vtest (true, s, _) | Vloop (_, s) | Vswitch (s,_) ->
+      begin match s.succs with
+        | [s'] -> block_scope s s'
+        | [] | _ :: _ ->
+            let s' = get_edge_next_stmt cfg e in
+            match s' with
+            | None -> no_scope
+            | Some s' -> block_scope s s'
+      end
+  | _ -> (* TODO ? *) no_scope
 
 let has_exit cfg =
   try
diff --git a/src/plugins/wp/cil2cfg.mli b/src/plugins/wp/cil2cfg.mli
index f0c16fe47c0b8bc779d8a83e55ee3d080aa0c9b0..5df3e524af058178dea5bb714a87eb04ca8cf994 100644
--- a/src/plugins/wp/cil2cfg.mli
+++ b/src/plugins/wp/cil2cfg.mli
@@ -107,7 +107,9 @@ val get_switch_edges : t -> node -> (exp list * edge) list * edge
     but gives the edge to VcallOut first and the edge to Vexit second. *)
 val get_call_out_edges : t -> node -> edge * edge
 
-val blocks_closed_by_edge : t -> edge -> block list
+type block_scope = { b_opened : block list ; b_closed : block list }
+
+val block_scope_for_edge : t -> edge -> block_scope
 
 val is_back_edge : edge -> bool
 
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
index 2c7f2a6b78db6f44db8d357ac2a058fdcd7988fb..d1e95f07802a37aca4d1c87ef2585aad84f75219 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_837.res.oracle
@@ -60,7 +60,6 @@ Prove: true.
 
 Goal Assigns nothing in 'foo' (4/4):
 Effect at line 6
-Assume { Type: is_sint32(a). (* Residual *) When: a != 0. }
-Prove: (ta_tmp_0=false).
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
index a619021a1b9190554575130a51912421d49b3730..1e55e4e4da4d50a375b1d5045388b3b665121725 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_837.res.oracle
@@ -12,12 +12,11 @@
 [wp] [Qed] Goal typed_foo_assigns_part1 : Valid
 [wp] [Qed] Goal typed_foo_assigns_part2 : Valid
 [wp] [Qed] Goal typed_foo_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assigns_part4 : Unsuccess
-[wp] Proved goals:    8 / 9
-  Qed:             8 
-  Alt-Ergo:        0  (unsuccess: 1)
+[wp] [Qed] Goal typed_foo_assigns_part4 : Valid
+[wp] Proved goals:    9 / 9
+  Qed:             9
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  foo                       3        -        4      75.0%
+  foo                       4        -        4       100%
   bar                       5        -        5       100%
 ------------------------------------------------------------