diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index 39b59cd426aa54145b25cf23dbd39b524abe6358..6661a8ddf21a976e0af492d6de048f1fd766eb88 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -216,15 +216,6 @@ struct
 
 end
 
-module Mode(OPT : sig val get : unit -> bool end) =
-struct
-  let default = OPT.get
-  let merge a b = if default () then a && b else a || b
-end
-
-module RW = Mode(Wp.Region_rw)
-module Flat = Mode(Wp.Region_flat)
-module Pack = Mode(Wp.Region_pack)
 
 (* -------------------------------------------------------------------------- *)
 (* --- Data Layout                                                        --- *)
diff --git a/src/plugins/wp/Layout.mli b/src/plugins/wp/Layout.mli
index 5370aa2299e1ca43c79644f52c12c27e6815f7ac..1db68dd9fa0d75eb25f20a5d3b97a0f49f655595 100644
--- a/src/plugins/wp/Layout.mli
+++ b/src/plugins/wp/Layout.mli
@@ -261,25 +261,4 @@ end
 (** {2 Options} *)
 (* -------------------------------------------------------------------------- *)
 
-(** Read-Write access *)
-module RW :
-sig
-  val default : unit -> bool
-  val merge : bool -> bool -> bool
-end
-
-(** Flatten arrays *)
-module Flat :
-sig
-  val default : unit -> bool
-  val merge : bool -> bool -> bool
-end
-
-(** Pack fields *)
-module Pack :
-sig
-  val default : unit -> bool
-  val merge : bool -> bool -> bool
-end
-
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index a0334d13b33e70c17d25d9fb35223a6788ed728d..9268c9e87a80e682a9c5a7c346a9a1c04da61d68 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -284,95 +284,6 @@ module Volatile =
                 Use -wp-no-volatile to ignore volatile attributes."
   end)
 
-(* -------------------------------------------------------------------------- *)
-(* --- Region Model                                                       --- *)
-(* -------------------------------------------------------------------------- *)
-
-let wp_region = add_group "Region Analysis"
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region =
-  False
-    (struct
-      let option_name = "-wp-region"
-      let help = "Perform Region Analysis (experimental)"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_fixpoint =
-  True
-    (struct
-      let option_name = "-wp-region-fixpoint"
-      let help = "Compute region aliasing fixpoint"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_cluster =
-  True
-    (struct
-      let option_name = "-wp-region-cluster"
-      let help = "Compute region clustering fixpoint"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_inline =
-  True
-    (struct
-      let option_name = "-wp-region-inline"
-      let help = "Inline aliased sub-clusters"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_rw =
-  True
-    (struct
-      let option_name = "-wp-region-rw"
-      let help = "Written region are considered read-write by default"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_pack =
-  True
-    (struct
-      let option_name = "-wp-region-pack"
-      let help = "Pack clusters by default"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_flat =
-  False
-    (struct
-      let option_name = "-wp-region-flat"
-      let help = "Flatten arrays by default"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-module Region_annot =
-  False
-    (struct
-      let option_name = "-region-annot"
-      let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
-    end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.is_invisible ()
-module Region_output_dot =
-  Filepath
-    (struct
-      let option_name = "-wp-region-output-dot"
-      let arg_name = "output.dot"
-      let file_kind = "DOT"
-      let existence = Fc_Filepath.Indifferent
-      let help = "Outputs the region graph in DOT format to the specified file."
-    end)
-
 (* ------------------------------------------------------------------------ *)
 (* ---  WP Strategy                                                     --- *)
 (* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 5c5159c59b555de8425115b69d7971a89c18ec07..84a25a418c36a8b3ca43d84f4b195aeb76505873 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -64,16 +64,6 @@ module Literals : Parameter_sig.Bool
 module Volatile : Parameter_sig.Bool
 module WeakIntModel : Parameter_sig.Bool
 
-module Region: Parameter_sig.Bool
-module Region_rw: Parameter_sig.Bool
-module Region_pack: Parameter_sig.Bool
-module Region_flat: Parameter_sig.Bool
-module Region_annot: Parameter_sig.Bool
-module Region_inline: Parameter_sig.Bool
-module Region_fixpoint: Parameter_sig.Bool
-module Region_cluster: Parameter_sig.Bool
-module Region_output_dot : Parameter_sig.Filepath
-
 (** {2 Computation Strategies} *)
 
 module Init: Parameter_sig.Bool