diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 0d03366f1..6c8e330be 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -61,24 +61,27 @@ module SymLinear = struct
     (singleton_one lb, singleton_one ub)
 
 
-  let pp1 : is_beginning:bool -> F.formatter -> Symb.Symbol.t -> NonZeroInt.t -> unit =
-   fun ~is_beginning f s c ->
+  let pp1 :
+      markup:bool -> is_beginning:bool -> F.formatter -> Symb.Symbol.t -> NonZeroInt.t -> unit =
+   fun ~markup ~is_beginning f s c ->
     let c = (c :> Z.t) in
     let c =
       if is_beginning then c
       else if Z.gt c Z.zero then ( F.pp_print_string f " + " ; c )
       else ( F.pp_print_string f " - " ; Z.neg c )
     in
-    if Z.(equal c one) then Symb.Symbol.pp f s
-    else if Z.(equal c minus_one) then F.fprintf f "-%a" Symb.Symbol.pp s
-    else F.fprintf f "%a%s%a" Z.pp_print c SpecialChars.dot_operator Symb.Symbol.pp s
+    if Z.(equal c one) then (Symb.Symbol.pp_mark ~markup) f s
+    else if Z.(equal c minus_one) then F.fprintf f "-%a" (Symb.Symbol.pp_mark ~markup) s
+    else
+      F.fprintf f "%a%s%a" Z.pp_print c SpecialChars.dot_operator (Symb.Symbol.pp_mark ~markup) s
 
 
-  let pp : is_beginning:bool -> F.formatter -> t -> unit =
-   fun ~is_beginning f x ->
+  let pp : markup:bool -> is_beginning:bool -> F.formatter -> t -> unit =
+   fun ~markup ~is_beginning f x ->
     if M.is_empty x then if is_beginning then F.pp_print_string f "0" else ()
     else
-      (M.fold (fun s c is_beginning -> pp1 ~is_beginning f s c ; false) x is_beginning : bool)
+      ( M.fold (fun s c is_beginning -> pp1 ~markup ~is_beginning f s c ; false) x is_beginning
+        : bool )
       |> ignore
 
 
@@ -233,8 +236,8 @@ module Bound = struct
 
   let equal = [%compare.equal: t]
 
-  let pp : F.formatter -> t -> unit =
-   fun f -> function
+  let pp_mark : markup:bool -> F.formatter -> t -> unit =
+   fun ~markup f -> function
     | MInf ->
         F.pp_print_string f "-oo"
     | PInf ->
@@ -242,15 +245,17 @@ module Bound = struct
     | Linear (c, x) ->
         if SymLinear.is_zero x then Z.pp_print f c
         else (
-          SymLinear.pp ~is_beginning:true f x ;
+          SymLinear.pp ~markup ~is_beginning:true f x ;
           if not Z.(equal c zero) then
             if Z.gt c Z.zero then F.fprintf f " + %a" Z.pp_print c
             else F.fprintf f " - %a" Z.pp_print (Z.neg c) )
     | MinMax (c, sign, m, d, x) ->
         if Z.(equal c zero) then (Sign.pp ~need_plus:false) f sign
         else F.fprintf f "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ;
-        F.fprintf f "%a(%a, %a)" MinMax.pp m Z.pp_print d Symb.Symbol.pp x
+        F.fprintf f "%a(%a, %a)" MinMax.pp m Z.pp_print d (Symb.Symbol.pp_mark ~markup) x
+
 
+  let pp = pp_mark ~markup:false
 
   let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf
 
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index c164b4437..e2500d031 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -43,6 +43,8 @@ module Bound : sig
 
   val pp : F.formatter -> t -> unit
 
+  val pp_mark : markup:bool -> F.formatter -> t -> unit
+
   val of_int : int -> t
 
   val of_big_int : Z.t -> t
diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 354365f69..0e0881ea0 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -785,15 +785,15 @@ module Report = struct
    fun summary cond_set ->
     let report cond trace issue_type =
       let location = PO.ConditionTrace.get_report_location trace in
-      let description = PO.description cond trace in
+      let description ~markup = PO.description ~markup cond trace in
       let trace =
         match TraceSet.choose_shortest (PO.ConditionTrace.get_val_traces trace) with
         | trace ->
-            make_err_trace trace description
+            make_err_trace trace (description ~markup:false)
         | exception _ ->
-            [Errlog.make_trace_element 0 location description []]
+            [Errlog.make_trace_element 0 location (description ~markup:false) []]
       in
-      Reporting.log_error summary ~loc:location ~ltr:trace issue_type description
+      Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true)
     in
     PO.ConditionSet.check_all ~report cond_set
 
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 1458da44f..16c37c58e 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -24,7 +24,9 @@ module AllocSizeCondition = struct
 
   let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length
 
-  let pp_description fmt length = F.fprintf fmt "Length: %a" ItvPure.pp length
+  let pp_description ~markup fmt length =
+    F.fprintf fmt "Length: %a" (ItvPure.pp_mark ~markup) length
+
 
   let make ~length = if ItvPure.is_invalid length then None else Some length
 
@@ -126,18 +128,19 @@ module ArrayAccessCondition = struct
         Relation.SymExp.pp_opt c.size_sym_exp Relation.pp c.relation
 
 
-  let pp_description : F.formatter -> t -> unit =
-   fun fmt c ->
+  let pp_description : markup:bool -> F.formatter -> t -> unit =
+   fun ~markup fmt c ->
     let pp_offset fmt =
-      if ItvPure.is_zero c.offset then ItvPure.pp fmt c.idx
-      else if ItvPure.is_zero c.idx then ItvPure.pp fmt c.offset
+      if ItvPure.is_zero c.offset then ItvPure.pp_mark ~markup fmt c.idx
+      else if ItvPure.is_zero c.idx then ItvPure.pp_mark ~markup fmt c.offset
       else
-        F.fprintf fmt "%a (= %a + %a)" ItvPure.pp (ItvPure.plus c.offset c.idx) ItvPure.pp c.offset
-          ItvPure.pp c.idx
+        F.fprintf fmt "%a (%s %a + %a)" (ItvPure.pp_mark ~markup) (ItvPure.plus c.offset c.idx)
+          SpecialChars.leftwards_double_arrow (ItvPure.pp_mark ~markup) c.offset
+          (ItvPure.pp_mark ~markup) c.idx
     in
     F.fprintf fmt "Offset%s: %t Size: %a"
       (if c.is_collection_add then " added" else "")
-      pp_offset ItvPure.pp (ItvPure.make_positive c.size)
+      pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size)
 
 
   let make :
@@ -322,7 +325,14 @@ module BinaryOperationCondition = struct
 
   let equal_binop = [%compare.equal: binop_t]
 
-  let binop_to_string = function Plus -> "+" | Minus -> "-" | Mult -> "*"
+  let binop_to_string = function
+    | Plus ->
+        "+"
+    | Minus ->
+        "-"
+    | Mult ->
+        SpecialChars.multiplication_sign
+
 
   type t =
     { binop: binop_t
@@ -378,8 +388,9 @@ module BinaryOperationCondition = struct
           `NotComparable
 
 
-  let pp fmt {binop; typ; integer_widths; lhs; rhs} =
-    F.fprintf fmt "(%a %s %a):" ItvPure.pp lhs (binop_to_string binop) ItvPure.pp rhs ;
+  let pp_description ~markup fmt {binop; typ; integer_widths; lhs; rhs} =
+    F.fprintf fmt "(%a %s %a):" (ItvPure.pp_mark ~markup) lhs (binop_to_string binop)
+      (ItvPure.pp_mark ~markup) rhs ;
     match typ with
     | Typ.IBool ->
         F.fprintf fmt "bool"
@@ -389,7 +400,7 @@ module BinaryOperationCondition = struct
           (Typ.width_of_ikind integer_widths typ)
 
 
-  let pp_description = pp
+  let pp = pp_description ~markup:false
 
   let is_mult_one binop lhs rhs =
     equal_binop binop Mult && (ItvPure.is_one lhs || ItvPure.is_one rhs)
@@ -549,13 +560,13 @@ module Condition = struct
         BinaryOperationCondition.pp fmt c
 
 
-  let pp_description fmt = function
+  let pp_description ~markup fmt = function
     | AllocSize c ->
-        AllocSizeCondition.pp_description fmt c
+        AllocSizeCondition.pp_description ~markup fmt c
     | ArrayAccess c ->
-        ArrayAccessCondition.pp_description fmt c
+        ArrayAccessCondition.pp_description ~markup fmt c
     | BinaryOperation c ->
-        BinaryOperationCondition.pp_description fmt c
+        BinaryOperationCondition.pp_description ~markup fmt c
 
 
   let check = function
@@ -867,5 +878,5 @@ module ConditionSet = struct
    fun condset -> List.map condset ~f:ConditionWithTrace.for_summary
 end
 
-let description cond trace =
-  F.asprintf "%a%a" Condition.pp_description cond ConditionTrace.pp_description trace
+let description ~markup cond trace =
+  F.asprintf "%a%a" (Condition.pp_description ~markup) cond ConditionTrace.pp_description trace
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
index 1f7b64611..4ea473aed 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli
@@ -78,4 +78,4 @@ module ConditionSet : sig
   val forget_locs : AbsLoc.PowLoc.t -> t -> t
 end
 
-val description : Condition.t -> ConditionTrace.t -> string
+val description : markup:bool -> Condition.t -> ConditionTrace.t -> string
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 0d9d324ae..6daad39cc 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -385,6 +385,7 @@ module NonNegativePolynomial = struct
   let top_lifted_increasing ~f p1 p2 =
     match (p1, p2) with Top, _ | _, Top -> Top | NonTop p1, NonTop p2 -> NonTop (f p1 p2)
 
+
   let plus = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.plus
 
   let mult = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.mult
@@ -520,16 +521,18 @@ module ItvPure = struct
    fun ~prev:(l1, u1) ~next:(l2, u2) ~num_iters:_ -> (Bound.widen_l l1 l2, Bound.widen_u u1 u2)
 
 
-  let pp : F.formatter -> t -> unit =
-   fun fmt (l, u) ->
-    if Bound.equal l u then Bound.pp fmt l
+  let pp_mark : markup:bool -> F.formatter -> t -> unit =
+   fun ~markup fmt (l, u) ->
+    if Bound.equal l u then Bound.pp_mark ~markup fmt l
     else
       match Bound.is_same_symbol l u with
       | Some symbol when Config.bo_debug < 3 ->
-          Symb.SymbolPath.pp fmt symbol
+          Symb.SymbolPath.pp_mark ~markup fmt symbol
       | _ ->
-          F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u
+          F.fprintf fmt "[%a, %a]" (Bound.pp_mark ~markup) l (Bound.pp_mark ~markup) u
+
 
+  let pp = pp_mark ~markup:false
 
   let of_bound bound = (bound, bound)
 
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 4e5cca5a7..2e36fb2f4 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -62,6 +62,8 @@ module ItvPure : sig
 
   val pp : F.formatter -> t -> unit
 
+  val pp_mark : markup:bool -> F.formatter -> t -> unit
+
   val mone : t
 
   val zero : t
diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml
index 89136fe88..9e3c882de 100644
--- a/infer/src/bufferoverrun/symb.ml
+++ b/infer/src/bufferoverrun/symb.ml
@@ -67,6 +67,9 @@ module SymbolPath = struct
     (* unsound but avoids many FPs for non-array pointers *)
     | Field (_, p) ->
         represents_multiple_values p
+
+
+  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 end
 
 module Symbol = struct
@@ -98,6 +101,8 @@ module Symbol = struct
       F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id
 
 
+  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
+
   let is_unsigned : t -> bool = fun x -> x.unsigned
 
   let path {path} = path
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index 10f817dd9..92e6f1ba7 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/infer/src/bufferoverrun/symb.mli
@@ -25,7 +25,7 @@ module SymbolPath : sig
 
   type t = private Normal of partial | Offset of partial | Length of partial
 
-  val pp : F.formatter -> t -> unit
+  val pp_mark : markup:bool -> F.formatter -> t -> unit
 
   val pp_partial : F.formatter -> partial -> unit
 
@@ -53,7 +53,7 @@ module Symbol : sig
 
   val is_unsigned : t -> bool
 
-  val pp : F.formatter -> t -> unit
+  val pp_mark : markup:bool -> F.formatter -> t -> unit
 
   val equal : t -> t -> bool
 
diff --git a/infer/src/istd/SpecialChars.ml b/infer/src/istd/SpecialChars.ml
index 4cc1dba94..e61f363e6 100644
--- a/infer/src/istd/SpecialChars.ml
+++ b/infer/src/istd/SpecialChars.ml
@@ -32,3 +32,6 @@ let right_tack = if utf8 then "⊢" else "|-"
 let superscript_digits =
   if utf8 then ("", [|"⁰"; "¹"; "²"; "³"; "⁴"; "⁵"; "⁶"; "⁷"; "⁸"; "⁹"|])
   else ("^", [|"0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"|])
+
+
+let leftwards_double_arrow = if utf8 then "⇐" else "<="
diff --git a/infer/src/istd/SpecialChars.mli b/infer/src/istd/SpecialChars.mli
index e6cd769ae..6225b57ff 100644
--- a/infer/src/istd/SpecialChars.mli
+++ b/infer/src/istd/SpecialChars.mli
@@ -14,3 +14,5 @@ val multiplication_sign : string
 val right_tack : string
 
 val superscript_digits : string * string Array.t
+
+val leftwards_double_arrow : string
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index dc3772a4b..97c1208a3 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -10,7 +10,7 @@ codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_b
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (2000000000 + 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_l2_Bad, 7, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Assignment,Binop: ([0, 2000000000] + [0, 2000000000]):signed32]
-codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (300000 * 300000):signed32]
+codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (300000 × 300000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_multiplication_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-2000000000 - 2000000000):signed32]
 codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_subtraction_Bad, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@@ -19,13 +19,13 @@ codetoanalyze/c/bufferoverrun/arith.c, minus_minimum_Bad, 2, INTEGER_OVERFLOW_L1
 codetoanalyze/c/bufferoverrun/arith.c, minus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([0, +oo] - 1):unsigned64]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
 codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: 5]
-codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] * 2):unsigned64]
-codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-1 * -9223372036854775808):signed64]
+codetoanalyze/c/bufferoverrun/arith.c, muliply_two_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_uint,Assignment,Binop: ([-oo, +oo] × 2):unsigned64]
+codetoanalyze/c/bufferoverrun/arith.c, mult_minimum_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (-1 × -9223372036854775808):signed64]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, plus_one_Bad, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: unknown_int,Assignment,Binop: ([-oo, 9223372036854775807] + 1):signed64]
-codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binop: (85 * 4294967295):unsigned32]
+codetoanalyze/c/bufferoverrun/arith.c, simple_overflow_Bad, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Binop: (85 × 4294967295):unsigned32]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
@@ -81,9 +81,9 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWA
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] * 4):unsigned64]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([5, +oo] × 4):unsigned64]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,Binop: ([0, +oo] + 5):signed32]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] * 10):signed32]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, False_Issue_Type_l3_unknown_function_Bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Assignment,Assignment,Return,ArrayDeclaration,Assignment,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: [5, +oo]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Alloc: Length: 2000000000]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Alloc: Length: -2]
@@ -101,7 +101,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [max(10, i), i] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [i, min(-1, i)] Size: 10]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] * 10):signed32]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: unknown_function,Binop: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: unknown_function,Assignment,ArrayAccess: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [-1, 9] Size: 9]
@@ -152,10 +152,10 @@ codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop4_Bad, 6, BUFFER_OVERRUN
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] (= [0, 1020] + [3, 1023]) Size: 1024]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 (= 5 + 5) Size: 10]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 (= 100 + -90) Size: 5 by call to `pointer_arith3` ]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 (= 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 10 (⇐ 5 + 5) Size: 10]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index 787f7114c..d0f1436f2 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -28,10 +28,10 @@ codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad,
 codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: (1 - [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: lib,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 30 Size: 10]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [1, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [1, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 0 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
-codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [1, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Return,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [1, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 5]
@@ -43,8 +43,8 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFE
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 5 by call to `plus_params2` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: -1 Size: 5 by call to `plus_params` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Assignment,Call,Assignment,Return,Assignment,ArrayDeclaration,Assignment,Assignment,ArrayAccess: Offset: 5 Size: [0, 6]]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
-codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] (= [0, +oo] + 2) Size: 12]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: data,Assignment,ArrayAccess: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
+codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Assignment,ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,ArrayAccess: Offset: [0, +oo] Size: 5 by call to `loop` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params2` ]
 codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: 11 Size: 5 by call to `plus_params` ]
@@ -53,18 +53,18 @@ codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Return,Binop: ([-oo, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter: this[*].infer_size,Assignment,Return,Assignment,Return,Assignment,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Parameter: this[*].infer_size,Assignment,Return,Assignment,Return,Assignment,Binop: ([-oo, +oo] - 1):signed32]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter: bi,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter: t[*].bI,Call,Parameter: t[*].bI,Call,Parameter: bi,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter: t[*].bI,Call,Parameter: t[*].bI,Call,Parameter: bi,Binop: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
 codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: v[*]._size,Call,Parameter: this[*]._size,Call,Parameter: this[*]._size,ArrayDeclaration,Assignment,Parameter: i,ArrayAccess: Offset: v[*]._size Size: v[*]._size by call to `int_vector_access_at` ]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 4611686018427387903]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 9223372036854775807]
-codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 9223372036854775807):unsigned64]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 × 9223372036854775807):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Alloc: Length: 18446744073709551615]
-codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 * 18446744073709551615):unsigned64]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Assignment,Binop: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Parameter: this[*].h,ArrayAccess: Offset: 10 Size: 10]
@@ -74,12 +74,12 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 4 Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter: __n,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Return,Assignment,Call,Return,Return,ArrayAccess: Offset: [-oo, +oo] Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([0, +oo] + 1):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: ([3, +oo] + 42):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,Parameter: __il,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 * [0, +oo]):unsigned64]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Binop: (4 × [0, +oo]):unsigned64]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter: __n,Assignment,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: 1 Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter: v[*].infer_size,Call,Parameter: this[*].infer_size,Call,Parameter: __n,Call,Parameter: this[*].infer_size,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: v[*].infer_size Size: v[*].infer_size]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: init,Assignment,Call,Parameter: __param_0[*].a,Assignment,Call,Parameter: count,Call,Parameter: this[*].a,Assignment,Return,ArrayAccess: Offset: -1 Size: 10 by call to `access_minus_one` ]
diff --git a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4 b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4
index ad4831b11..f4c2a73ae 100644
--- a/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4
+++ b/infer/tests/codetoanalyze/cpp/quandaryBO/issues.exp-t4
@@ -1,10 +1,10 @@
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a,Binop: (a * b):unsigned32]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a,Binop: (a × b):unsigned32]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::checkedMultiply_Good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Binop: ([0, +oo] * 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::foo_Bad_FN, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Binop: ([0, +oo] × 4):unsigned64 by call to `Codec_Bad2::getP_Bad` ]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad2::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: w,Assignment,Assignment,Assignment,Binop: ([-oo, +oo] + 1):unsigned64]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 4, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Call,Parameter: w,Assignment,Binop: ([0, +oo] - 1):unsigned32 by call to `Codec_Bad::getP_Bad` ]
-codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Binop: ([-oo, +oo] * [-oo, +oo]):unsigned32]
+codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::foo_Bad_FN, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Unknown value from: __infer_taint_source,Assignment,Binop: ([-oo, +oo] × [-oo, +oo]):unsigned32]
 codetoanalyze/cpp/quandaryBO/codec.cpp, Codec_Bad::getP_Bad, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: w,Assignment,Assignment,Assignment,Binop: ([-oo, +oo] + 1):unsigned32]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10]
 codetoanalyze/cpp/quandaryBO/tainted_index.cpp, basic_bad, 3, TAINTED_BUFFER_ACCESS, no_bucket, ERROR, [Return from __infer_taint_source,Call to __array_access with tainted index 0,-----------,ArrayDeclaration,Unknown value from: __infer_taint_source,Assignment,ArrayAccess: Offset: [-oo, +oo] Size: 10]
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 24993c432..dd2fa557b 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -130,7 +130,7 @@ codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.
 codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] (= [-oo, +oo] + [0, +oo]) Size: [0, +oo]]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: char[] String.toCharArray(),Assignment,Assignment,ArrayAccess: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [0, +oo]) Size: [0, +oo]]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Binop: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
@@ -144,7 +144,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a[*],Binop: (a[*] * b[*]):signed64]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter: a[*],Binop: (a[*] × b[*]):signed64]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]