diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index ae7c843b8..9fae1894f 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -986,6 +986,8 @@ module Reachability = struct
 
   let equal = M.equal
 
+  let pp = M.pp
+
   (* It keeps only symbolic pruned values, because non-symbolic ones are useless to see the
      reachability. *)
   let add v x = if PrunedVal.is_symbolic v then M.add v x else x
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 60e1f0882..1803d366e 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -708,10 +708,16 @@ module ConditionWithTrace = struct
     {cond; trace; reported= None; reachability= Dom.Reachability.make latest_prune}
 
 
-  let pp fmt {cond; trace} = F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace
+  let pp fmt {cond; trace; reachability} =
+    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp trace ;
+    if Config.bo_debug >= 3 then
+      F.fprintf fmt " reachable when %a" Dom.Reachability.pp reachability
 
-  let pp_summary fmt {cond; trace} =
-    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp_summary trace
+
+  let pp_summary fmt {cond; trace; reachability} =
+    F.fprintf fmt "%a %a" Condition.pp cond ConditionTrace.pp_summary trace ;
+    if Config.bo_debug >= 3 then
+      F.fprintf fmt " reachable when %a" Dom.Reachability.pp reachability
 
 
   let have_same_bounds {cond= cond1} {cond= cond2} = Condition.equal cond1 cond2