diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
index 4c912d7a61bcbfd7893dcb9ff18e129dd83b7e4a..f236171a3028096c948ed6c465f9bab4a979becd 100644
--- a/src/plugins/region/Region.ml
+++ b/src/plugins/region/Region.ml
@@ -36,6 +36,7 @@ let nodes = Memory.nodes
 let equal = Memory.equal
 let included = Memory.included
 let separated = Memory.separated
+let size = Memory.size
 let roots = Memory.roots
 let labels = Memory.labels
 let reads = Memory.reads
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
index baedc6b4030b073eddaee46908fcb1dc5c5fe1bf..c17d49d53195ff92cb7185c9d0118f1d2a898759 100644
--- a/src/plugins/region/Region.mli
+++ b/src/plugins/region/Region.mli
@@ -74,6 +74,8 @@ val nodes : map -> node list -> node list
 
 val points_to : map -> node -> node option
 val pointed_by : map -> node -> node list
+
+val size : map -> node -> int
 val parents : map -> node -> node list
 val roots : map -> node -> varinfo list
 val labels: map -> node -> string list
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 048e7ed6ee168efe62f0733a486774b341736a92..bc2916eaa1e2a85277379de15640f05eba511f5d 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -353,7 +353,10 @@ let regions map =
   iter map (fun r -> pool := region map r :: !pool) ;
   List.rev !pool
 
-let parents (m: map) (r: node) =
+let size (m: map) (r: node) =
+  sizeof (Ufind.get m.store r).clayout
+
+  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/region/memory.mli b/src/plugins/region/memory.mli
index 4e8f5c4da4b5c8897d0cb46a6eea0d467318f6a2..5485a5c974f8b2fae7c525d2077d0ab0a246c5d3 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -70,12 +70,13 @@ val equal : map -> node -> node -> bool
 val node : map -> node -> node
 val nodes : map -> node list -> node list
 
-val iter : map -> (node -> unit) -> unit
-val region : map -> node -> region
-val regions : map -> region list
+val size : map -> node -> int
 val parents : map -> node -> node list
 val roots : map -> node -> varinfo list
 val labels : map -> node -> string list
+val region : map -> node -> region
+val regions : map -> region list
+val iter : map -> (node -> unit) -> unit
 
 val new_chunk : map -> ?size:int -> ?ptr:node -> ?pointed:node -> unit -> node
 val add_root : map -> Cil_types.varinfo -> node
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
index 53cbfdca051c3276167945a14ef1256caa8b008b..ec894b8dfe1a1631719f09fbef5167b13a23d405 100644
--- a/src/plugins/wp/RegionAnalysis.ml
+++ b/src/plugins/wp/RegionAnalysis.ml
@@ -46,11 +46,10 @@ struct
   let pretty fmt r = Format.fprintf fmt "R%03d" @@ Region.id r
 end
 
-let types r =
+let types map r =
   let module Tset = Cil_datatype.Typ.Set in
   let pool = ref Tset.empty in
   let add ty = pool := Tset.add ty !pool in
-  let map = get_map () in
   List.iter add @@ Region.reads map r ;
   List.iter add @@ Region.writes map r ;
   List.iter add @@ Region.shifts map r ;
@@ -63,10 +62,11 @@ module Kind = WpContext.Generator(Type)
       type key = region
       type data = MemRegion.kind
       let name = "Wp.RegionAnalysis.R"
-      let compile region =
+      let compile r =
         let open MemRegion in
-        match types region with
-        | [ty] ->
+        let map = get_map () in
+        match types map r with
+        | [ty] when Cil.bitsSizeOf ty >= Region.size map r ->
           begin
             match Ctypes.object_of ty with
             | C_int i -> Many (Int i)