diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index bc2916eaa1e2a85277379de15640f05eba511f5d..1a51e063d1a6ac70f11c147d11d4294039137c95 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -356,7 +356,7 @@ let regions map =
 let size (m: map) (r: node) =
   sizeof (Ufind.get m.store r).clayout
 
-  let parents (m: map) (r: node) =
+let parents (m: map) (r: node) =
   nodes m (Ufind.get m.store r).cparents
 
 let roots (m: map) (r: node) =
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 025333ff770a4290474341b3fdeca557bcd2426a..76db5a5f0787e2150ff4c37dc546566a36a68b7f 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -59,6 +59,7 @@ sig
   val id : region -> int
   val of_id : int -> region option
   val kind : region -> kind
+  val name : region -> string option
   val cvar : varinfo -> region option
   val field : region -> fieldinfo -> region option
   val shift : region -> c_object -> region option
@@ -146,12 +147,15 @@ struct
       | Array p -> Qed.Logic.Array(MemAddr.t_addr,tau_of_prim p)
       | ArrInit -> Qed.Logic.Array(MemAddr.t_addr,Qed.Logic.Bool)
 
-    let basename_of_chunk { mu } =
+    let basename_of_chunk { mu ; region } =
       match mu with
-      | Value p -> Format.asprintf "V%a" pp_prim p
-      | Array p -> Format.asprintf "M%a" pp_prim p
       | ValInit -> "Vinit"
       | ArrInit -> "Minit"
+      | Array p -> Format.asprintf "M%a" pp_prim p
+      | Value p ->
+        match R.name region with
+        | Some a -> a
+        | None -> Format.asprintf "V%a" pp_prim p
 
     let is_framed _ = false
 
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 8bffdeab36c093d661c01da0aad551c53fee1c2a..545e03ac004fff4c80fce87a0cb2b1ad1e9066eb 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -40,6 +40,7 @@ sig
   val id : region -> int
   val of_id : int -> region option
   val kind : region -> kind
+  val name : region -> string option
   val cvar : varinfo -> region option
   val field : region -> fieldinfo -> region option
   val shift : region -> c_object -> region option
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index ec894b8dfe1a1631719f09fbef5167b13a23d405..aa173e616e704583942284c957949188fdc2e7ee 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -55,29 +55,53 @@ let types map r =
   List.iter add @@ Region.shifts map r ;
   Tset.elements !pool
 
+let rec singleton map r =
+  match Region.parents map r with
+  | [] -> List.length @@ Region.roots map r = 1
+  | [r] -> Region.roots map r = [] && singleton map r
+  | _ -> false
+
 (* Keeping track of the decision to apply which memory model to each region *)
 module Kind = WpContext.Generator(Type)
     (struct
       (* Data : WpContext.Data with type key = Key.t *)
       type key = region
       type data = MemRegion.kind
-      let name = "Wp.RegionAnalysis.R"
+      let name = "Wp.RegionAnalysis.Kind"
       let compile r =
         let open MemRegion in
         let map = get_map () in
         match types map r with
         | [ty] when Cil.bitsSizeOf ty >= Region.size map r ->
           begin
+            let pkind p = if singleton map r then Single p else Many p in
             match Ctypes.object_of ty with
-            | C_int i -> Many (Int i)
-            | C_float f -> Many (Float f)
-            | C_pointer _ -> Many Ptr
+            | C_int i -> pkind (Int i)
+            | C_float f -> pkind (Float f)
+            | C_pointer _ -> pkind Ptr
             | _ -> Garbled
           end
         | _ -> Garbled
     end)
 
+module Name = WpContext.Generator(Type)
+    (struct
+      (* Data : WpContext.Data with type key = Key.t *)
+      type key = region
+      type data = string option
+      let name = "Wp.RegionAnalysis.Name"
+      let compile r =
+        let map = get_map () in
+        match Region.labels map r with
+        | label::_ -> Some label
+        | [] ->
+          match Region.roots map r with
+          | v::_ -> Some v.vorig_name
+          | _ -> None
+    end)
+
 let kind = Kind.get
+let name = Name.get
 let points_to region = Region.points_to (get_map ()) region
 let separated r1 r2 = Region.separated (get_map ()) r1 r2
 let included r1 r2 = Region.included (get_map ()) r1 r2
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
index 2a9c0dd092977b12608e546e48164b8deb1d89df..9e615df719c8f1a9aeee600b0d66b123215e5393 100644
--- a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
@@ -11,19 +11,17 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file swap.i, line 20) in 'swap_aliased':
-Let a = Mptr_1[global(P_b_33)].
-Let a_1 = Mptr_0[global(P_a_32)].
-Let x = Msint32_0[a_1].
-Let x_1 = Msint32_0[a].
-Let x_2 = Msint32_0[a_1 <- x_1][a <- x][a_1].
+Let x = Msint32_0[a].
+Let x_1 = Msint32_0[b].
+Let x_2 = Msint32_0[a <- x_1][b <- x][a].
 Assume {
   Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
   (* Heap *)
-  Type: linked(alloc_0) /\ framed(Mptr_0) /\ framed(Mptr_1).
-  (* Pre-condition *)
-  Have: valid_rw(alloc_0, a_1, 4).
+  Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(alloc_0).
   (* Pre-condition *)
   Have: valid_rw(alloc_0, a, 4).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, b, 4).
 }
 Prove: x_2 = x_1.