[inferbo] Do not join traces if Prune changed nothing

Reviewed By: skcho

Differential Revision: D13176164

fbshipit-source-id: 35341a99e

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
+    let itv = f x.itv y.itv in
-      { x with
+    let arrayblk = g x.arrayblk y.arrayblk in
-        itv= f x.itv y.itv
+    if phys_equal itv x.itv && phys_equal arrayblk x.arrayblk then
-      ; arrayblk= g x.arrayblk y.arrayblk
+      (* x hasn't changed, don't join traces *)
-      ; traces= TraceSet.join x.traces y.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