From b92800a716d04f7b09d1d9f94dfbbf061089ade7 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Mon, 26 Nov 2018 13:49:08 -0800
Subject: [PATCH] [inferbo] Do not join traces if Prune changed nothing

Reviewed By: skcho

Differential Revision: D13176164

fbshipit-source-id: 35341a99e
---
 infer/src/bufferoverrun/bufferOverrunDomain.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index ab4b641f1..9bffdc6e4 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -257,11 +257,14 @@ module Val = struct
   let lift_prune2 :
       (Itv.t -> Itv.t -> Itv.t) -> (ArrayBlk.t -> ArrayBlk.t -> ArrayBlk.t) -> t -> t -> t =
    fun f g x y ->
-    warn_against_pruning_multiple_values
-      { x with
-        itv= f x.itv y.itv
-      ; arrayblk= g x.arrayblk y.arrayblk
-      ; traces= TraceSet.join x.traces y.traces }
+    let itv = f x.itv y.itv in
+    let arrayblk = g x.arrayblk y.arrayblk in
+    if phys_equal itv x.itv && phys_equal arrayblk x.arrayblk then
+      (* x hasn't changed, don't join traces *)
+      x
+    else
+      warn_against_pruning_multiple_values
+        {x with itv; arrayblk; traces= TraceSet.join x.traces y.traces}
 
 
   let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero