diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index ba69ffcc2a1fc8876454475f345855976e8303fb..a60663c67ed3fd2a2213a97fae969467d931a3ba 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -76,12 +76,12 @@ module Cfg (W : Mcfg.S) = struct
   let add_assigns_hyp wenv obj h_assigns = match h_assigns with
     | WpPropId.AssignsLocations (h_id, a) ->
         let hid = Some h_id in
-        let obj = W.use_assigns wenv a.WpPropId.a_stmt hid a obj in
+        let obj = W.use_assigns wenv hid a obj in
         Some a.WpPropId.a_label, obj
     | WpPropId.AssignsAny a ->
         Wp_parameters.warning ~current:true ~once:true
           "Missing assigns clause (assigns 'everything' instead)" ;
-        let obj = W.use_assigns wenv a.WpPropId.a_stmt None a obj in
+        let obj = W.use_assigns wenv None a obj in
         Some a.WpPropId.a_label, obj
     | WpPropId.NoAssignsInfo -> None, obj
 
@@ -476,7 +476,7 @@ module Cfg (W : Mcfg.S) = struct
           | (Set (lv, e, _)) -> W.assign wenv s lv e obj
           | (Asm _) ->
               let asm = WpPropId.mk_asm_assigns_desc s in
-              W.use_assigns wenv asm.WpPropId.a_stmt None asm obj
+              W.use_assigns wenv None asm obj
           | (Call _) -> assert false
           | Skip _ | Code_annot _ -> obj
         end
@@ -652,7 +652,7 @@ module Cfg (W : Mcfg.S) = struct
         let obj =
           if WpStrategy.isInitConst ()
           then process_global_const wenv obj else obj in
-        let obj = W.use_assigns wenv None None WpPropId.mk_init_assigns obj in
+        let obj = W.use_assigns wenv None WpPropId.mk_init_assigns obj in
         let obj = W.label wenv None Clabels.init obj in
         compute_global_init wenv `All obj
       end
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index 6091b24dc5af8716fc40177bdbc5c32f852adfd5..24d85bc4505dd21849a889b3649d5a44b3a24b66 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -124,7 +124,7 @@ struct
     Format.fprintf !out "  %a -> %a [ style=dotted ] ;@." pretty u pretty k ;
     merge env u k
 
-  let use_assigns _env _stmt region d k =
+  let use_assigns _env region d k =
     let u = node () in
     begin match region with
       | None ->
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index fd9f7e1d95955cdd19f0f8978fcf56ba0bd51312..d8d221d9cbd5209bb9adca1d4105cd6ddfe3715d 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -598,9 +598,9 @@ struct
     let sequence = { pre=s0 ; post=s1 } in
     sequence , assigned
 
-  let use_assigns wenv stmt hpid ainfo wp = in_wenv wenv wp
+  let use_assigns wenv hpid ainfo wp = in_wenv wenv wp
       begin fun env wp ->
-        assert (stmt == ainfo.a_stmt) ;
+        let stmt = ainfo.a_stmt in
         match ainfo.a_assigns with
 
         | WritesAny ->
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.ml
index 873001be1ebceef7f7c3212b4b449f6f02319a6d..5fd7743b59ceaeb829524f7d285df1ab2fead0eb 100644
--- a/src/plugins/wp/mcfg.ml
+++ b/src/plugins/wp/mcfg.ml
@@ -73,8 +73,8 @@ module type S = sig
   (** [use_assigns env hid kind assgn goal] performs the havoc on the goal.
    * [hid] should be [None] iff [assgn] is [WritesAny],
    * and tied to the corresponding identified_property otherwise.*)
-  val use_assigns : t_env -> stmt option -> WpPropId.prop_id option ->
-    WpPropId.assigns_desc -> t_prop -> t_prop
+  val use_assigns : t_env ->
+    WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_prop
 
   val label  : t_env -> stmt option -> Clabels.c_label -> t_prop -> t_prop
   val init : t_env -> varinfo -> init option -> t_prop -> t_prop