diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 0846594ea..b10f8965e 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -829,17 +829,26 @@ module CoreVal = struct
 
   let compare x y =
     let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in
-    if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y)
+    if r <> 0 then r
+    else
+      let r = PowLoc.compare (Val.get_pow_loc x) (Val.get_pow_loc y) in
+      if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y)
+
 
+  let pp fmt x =
+    F.fprintf fmt "(%a, %a, %a)" Itv.pp (Val.get_itv x) PowLoc.pp (Val.get_pow_loc x) ArrayBlk.pp
+      (Val.get_array_blk x)
 
-  let pp fmt x = F.fprintf fmt "(%a, %a)" Itv.pp (Val.get_itv x) ArrayBlk.pp (Val.get_array_blk x)
 
   let is_symbolic v =
     let itv = Val.get_itv v in
     if Itv.is_bottom itv then ArrayBlk.is_symbolic (Val.get_array_blk v) else Itv.is_symbolic itv
 
 
-  let is_empty v = Itv.is_bottom (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v)
+  let is_empty v =
+    Itv.is_bottom (Val.get_itv v)
+    && PowLoc.is_empty (Val.get_pow_loc v)
+    && ArrayBlk.is_empty (Val.get_array_blk v)
 end
 
 module PruningExp = struct
@@ -968,6 +977,8 @@ module PrunePairs = struct
   include AbstractDomain.InvertedMap (Loc) (PrunedVal)
 
   let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
+
+  let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x)
 end
 
 module LatestPrune = struct
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 90ae73ff6..7fe10334f 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -664,7 +664,7 @@ module Prune = struct
       Mem.meet_constraints constrs mem
     in
     let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in
-    Mem.set_prune_pairs prune_pairs mem
+    if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.bot
 end
 
 let get_matching_pairs :