diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index dee4aee6f..6b33d0857 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -336,14 +336,21 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
     let pp_symbs fmt (last, others) =
       List.rev_append others [last] |> Pp.seq ~sep:" * " pp_symb_exp fmt
     in
-    let rec pp_sub symbs fmt {const; terms} =
-      if not (NonNegativeInt.is_zero const) then
-        F.fprintf fmt " + %a%a" pp_coeff const pp_symbs symbs ;
-      M.iter (fun s p -> pp_sub (add_symb s symbs) fmt p) terms
+    let rec pp_sub ~print_plus symbs fmt {const; terms} =
+      if not (NonNegativeInt.is_zero const) then (
+        if print_plus then F.pp_print_string fmt " + " ;
+        F.fprintf fmt "%a%a" pp_coeff const pp_symbs symbs ) ;
+      M.iter (fun s p -> pp_sub ~print_plus:true (add_symb s symbs) fmt p) terms
     in
     fun fmt {const; terms} ->
-      NonNegativeInt.pp fmt const ;
-      M.iter (fun s p -> pp_sub ((s, PositiveInt.one), []) fmt p) terms
+      let const_not_zero = not (NonNegativeInt.is_zero const) in
+      if const_not_zero || M.is_empty terms then NonNegativeInt.pp fmt const ;
+      M.fold
+        (fun s p print_plus ->
+          pp_sub ~print_plus ((s, PositiveInt.one), []) fmt p ;
+          true )
+        terms const_not_zero
+      |> ignore
 end
 
 module NonNegativePolynomial = struct