diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index a08b50fe7965b09c94c2454d73100d20130e0f5e..73d143221fc088811e7a54a4d23e947d0204563d 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -44,6 +44,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
   | _ :: _ ->
     old.labels <- [];
     new_stmt.labels <- labels @ new_stmt.labels;
+    let old = Cil.get_original_stmt vis#behavior old in
     Labeled_stmts.add old new_stmt;
     (* update the gotos of the function jumping to one of the labels *)
     let o orig_stmt = object
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1d570d703fdd8ed5fa0f7e235843e64ae1acf945..05cf6dfdf1243b96e6d0284c135f5e3a4ed1fbe9 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -678,10 +678,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
                 b.bstmts <- List.rev l @ delete_stmts
             end;
             let new_stmt = Misc.mk_block prj stmt b in
-            (* move the labels of the return to the new block in order to
-               evaluate the postcondition when jumping to them. *)
-            E_acsl_label.move
-              (self :> Visitor.generic_frama_c_visitor) stmt new_stmt;
+            if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
+              (* move the labels of the return to the new block in order to
+                 evaluate the postcondition when jumping to them. *)
+              E_acsl_label.move
+                (self :> Visitor.generic_frama_c_visitor) stmt new_stmt
+            end;
             new_stmt, env
           else
             stmt, env