diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index 9887ef2a37adedaa0dd9f83ae41780b95219e4be..89949e3c7276fac39a3bb4f6b455711f7cadb443 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -52,9 +52,9 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
       (* invariant of this method: [s = Cil.memo_stmt vis#behavior orig_stmt] *)
       method !vstmt_aux s = match s.skind, orig_stmt.skind with
       | Goto(s_ref, _), Goto(orig_ref, _) ->
-        if Cil_datatype.Stmt.equal !s_ref old && s_ref != orig_ref then
-          (* Forward goto: it has already been visited and there is no more
-             sharing. Must update the reference. *)
+        if Cil_datatype.Stmt.equal !orig_ref old && s_ref != orig_ref then
+          (* Forward goto: it has already been visited.
+             We must update the reference. *)
           s_ref := new_stmt;
         Cil.SkipChildren
       | _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 9726a521bee689857bd2b7265488e81523c350c2..db194ddf24c866de12f554363f968aaa1ca29651 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -663,8 +663,7 @@ and at_to_exp env t_opt label e =
   end
   in
   let bhv = Env.get_behavior new_env in
-  let new_stmt = Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt) in
-  Cil.set_stmt bhv stmt new_stmt;
+  ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
   res, !env_ref, false
 
 and env_of_li li kf env loc =
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c2c928a4161a4cf0c8eda024e23dd8f019704b0a..a65afdce47ad26dc91cf68a4f920aaf7bdab2e07 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -742,15 +742,13 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       in
       let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
       if not (may_safely_ignore lv) && must_model then
-        let before = Cil.memo_stmt self#behavior stmt in
+        let before = Cil.mkStmt stmt.skind in
         let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
-        let new_stmt = Cil.memo_stmt self#behavior new_stmt in
         let env = Env.add_stmt ~post ~before env new_stmt in
         let env = match vi with
           | None -> env
           | Some vi ->
             let new_stmt = Project.on prj Misc.mk_store_stmt vi in
-            let new_stmt = Cil.memo_stmt self#behavior new_stmt in
             Env.add_stmt ~post ~before env new_stmt
         in
         env
@@ -891,27 +889,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     end else
       Cil.SkipChildren
 
-  method !vterm _ =
-    Cil.DoChildrenPost
-      (fun t ->
-        (match t.term_node with
-        | Tat(_, StmtLabel s_ref) ->
-          (* the label may have been moved,
-             so move the corresponding reference *)
-          s_ref := E_acsl_label.new_labeled_stmt !s_ref
-        | _ -> ());
-        t)
-
-  method !vpredicate_node _ =
-    Cil.DoChildrenPost
-      (function
-      | Pat(_, StmtLabel s_ref) as p ->
-          (* the label may have been moved,
-             so move the corresponding reference *)
-        s_ref := E_acsl_label.new_labeled_stmt !s_ref;
-        p
-      | p -> p);
-
   initializer
     Misc.reset ();
     Literal_strings.reset ();