diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 411b76bf1f2ee11d866c3a86da1c4d399605c5c3..57458a5688878cb8930006420b56b818aa7905d5 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -496,18 +496,7 @@ class prepare_visitor = object (self)
          Annotations.iter_code_annot
            (fun _ a -> self#push_post_code_annot a)
            stmt;
-         (* move variables declared in the body of a switch statement to the
-            outer scope *)
-         match stmt.skind with
-         | Switch(_,sw_blk,_,_) ->
-           let new_blk = Cil.mkBlock [ stmt ] in
-           let new_stmt = Cil.mkStmt ~valid_sid:true (Block new_blk) in
-           new_blk.blocals <- sw_blk.blocals;
-           sw_blk.blocals <- [];
-           has_new_stmt_in_fundec <- true;
-           new_stmt
-         | _ ->
-           stmt)
+         stmt)
 
   method !vfunc fundec =
     Cil.DoChildrenPost
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index db215c119ea6d4cdf06ea56c2eed274293ce33ae..5237a7d39d59ca87564a0f4d6329972f641c9f42 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -25,8 +25,6 @@
     More precisely, this module performs the following tasks:
     - generating a new definition for functions with contract;
     - removing term sharing;
-    - moving declarations of variables declared in the bodies of switch
-      statements to upper scopes;
     - storing what is necessary to translate in [Keep_status];
     - in case of temporal validity checks, adding the attribute "aligned" to
       variables that are not sufficiently aligned. *)