diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml
index c17413a0e..aace3ae5e 100644
--- a/infer/src/absint/AbstractDomain.ml
+++ b/infer/src/absint/AbstractDomain.ml
@@ -12,6 +12,8 @@ module Types = struct
   type 'astate bottom_lifted = Bottom | NonBottom of 'astate
 
   type 'astate top_lifted = Top | NonTop of 'astate
+
+  type ('below, 'above) below_above = Below of 'below | Above of 'above
 end
 
 open! Types
@@ -250,6 +252,68 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct
   let get = function V v -> Some v | Bot | Top -> None
 end
 
+module StackedUtils = struct
+  let compare x1 x2 ~cmp_below ~cmp_above =
+    if phys_equal x1 x2 then 0
+    else
+      match (x1, x2) with
+      | Below b1, Below b2 ->
+          cmp_below b1 b2
+      | Below _, Above _ ->
+          -1
+      | Above _, Below _ ->
+          1
+      | Above a1, Above a2 ->
+          cmp_above a1 a2
+
+
+  let ( <= ) ~le_below ~le_above ~lhs ~rhs =
+    phys_equal lhs rhs
+    ||
+    match (lhs, rhs) with
+    | Below lhs, Below rhs ->
+        le_below ~lhs ~rhs
+    | Below _, Above _ ->
+        true
+    | Above _, Below _ ->
+        false
+    | Above lhs, Above rhs ->
+        le_above ~lhs ~rhs
+
+
+  let combine ~dir x1 x2 ~f_below ~f_above =
+    match (x1, x2) with
+    | Below b1, Below b2 ->
+        Below (f_below b1 b2)
+    | (Below _ as below), (Above _ as above) | (Above _ as above), (Below _ as below) -> (
+      match dir with `Increasing -> above | `Decreasing -> below )
+    | Above a1, Above a2 ->
+        Above (f_above a1 a2)
+
+
+  let map x ~f_below ~f_above =
+    match x with Below b -> Below (f_below b) | Above a -> Above (f_above a)
+
+
+  let pp ~pp_below ~pp_above f = function Below b -> pp_below f b | Above a -> pp_above f a
+end
+
+module Stacked (Below : S) (Above : S) = struct
+  type t = (Below.t, Above.t) below_above
+
+  let ( <= ) = StackedUtils.( <= ) ~le_below:Below.( <= ) ~le_above:Above.( <= )
+
+  let join = StackedUtils.combine ~dir:`Increasing ~f_below:Below.join ~f_above:Above.join
+
+  let widen ~prev ~next ~num_iters =
+    StackedUtils.combine ~dir:`Increasing prev next
+      ~f_below:(fun prev next -> Below.widen ~prev ~next ~num_iters)
+      ~f_above:(fun prev next -> Above.widen ~prev ~next ~num_iters)
+
+
+  let pp = StackedUtils.pp ~pp_below:Below.pp ~pp_above:Above.pp
+end
+
 module MinReprSet (Element : PrettyPrintable.PrintableOrderedType) = struct
   type elt = Element.t [@@deriving compare]
 
diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli
index 2a9b0925a..0ff8bfbc0 100644
--- a/infer/src/absint/AbstractDomain.mli
+++ b/infer/src/absint/AbstractDomain.mli
@@ -11,6 +11,8 @@ module Types : sig
   type 'astate bottom_lifted = Bottom | NonBottom of 'astate
 
   type 'astate top_lifted = Top | NonTop of 'astate
+
+  type ('below, 'above) below_above = Below of 'below | Above of 'above
 end
 
 open! Types
@@ -76,11 +78,7 @@ end
 module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted
 
 module TopLiftedUtils : sig
-  val ( <= ) : le:(lhs:'a -> rhs:'a -> bool) -> lhs:'a top_lifted -> rhs:'a top_lifted -> bool
-
   val pp_top : Format.formatter -> unit
-
-  val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a top_lifted -> unit
 end
 
 (** Cartesian product of two domains. *)
@@ -97,6 +95,48 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) : sig
   val get : t -> V.t option
 end
 
+include
+  sig
+    [@@@warning "-60"]
+
+    (** Stacked abstract domain: tagged union of [Below] and [Above] domains where all elements of [Below] are strictly smaller than elements of [Above] *)
+    module Stacked (Below : S) (Above : S) : S with type t = (Below.t, Above.t) below_above
+end
+
+module StackedUtils : sig
+  val ( <= ) :
+       le_below:(lhs:'b -> rhs:'b -> bool)
+    -> le_above:(lhs:'a -> rhs:'a -> bool)
+    -> lhs:('b, 'a) below_above
+    -> rhs:('b, 'a) below_above
+    -> bool
+
+  val compare :
+       ('b, 'a) below_above
+    -> ('b, 'a) below_above
+    -> cmp_below:('b -> 'b -> int)
+    -> cmp_above:('a -> 'a -> int)
+    -> int
+
+  val pp :
+       pp_below:(Format.formatter -> 'b -> unit)
+    -> pp_above:(Format.formatter -> 'a -> unit)
+    -> Format.formatter
+    -> ('b, 'a) below_above
+    -> unit
+
+  val combine :
+       dir:[`Increasing | `Decreasing]
+    -> ('b, 'a) below_above
+    -> ('b, 'a) below_above
+    -> f_below:('b -> 'b -> 'b)
+    -> f_above:('a -> 'a -> 'a)
+    -> ('b, 'a) below_above
+
+  val map :
+    ('b, 'a) below_above -> f_below:('b -> 'b2) -> f_above:('a -> 'a2) -> ('b2, 'a2) below_above
+end
+
 (** Abstracts a set of [Element]s by keeping its smallest representative only.
   The widening is terminating only if the order fulfills the descending chain condition. *)
 module MinReprSet (Element : PrettyPrintable.PrintableOrderedType) : sig
diff --git a/infer/src/backend/Differential.ml b/infer/src/backend/Differential.ml
index 9bdabeee8..31bb0eedf 100644
--- a/infer/src/backend/Differential.ml
+++ b/infer/src/backend/Differential.ml
@@ -175,18 +175,21 @@ let issue_of_cost cost_info ~delta ~prev_cost ~curr_cost =
     let line = cost_info.Jsonbug_t.loc.lnum in
     let column = cost_info.Jsonbug_t.loc.cnum in
     let trace =
+      let polynomial_traces =
+        match curr_degree_with_term with
+        | Below (_, degree_term) ->
+            Polynomials.NonNegativeNonTopPolynomial.get_symbols degree_term
+            |> List.map ~f:Bounds.NonNegativeBound.make_err_trace
+        | Above traces ->
+            [("", Polynomials.TopTraces.make_err_trace traces)]
+      in
       let curr_cost_trace =
         [ Errlog.make_trace_element 0
             {Location.line; col= column; file= source_file}
             (Format.asprintf "Updated %a" curr_cost_msg ())
             [] ]
       in
-      Option.value_map ~default:curr_cost_trace
-        ~f:(fun (_, degree_term) ->
-          let symbol_list = Polynomials.NonNegativeNonTopPolynomial.get_symbols degree_term in
-          ("", curr_cost_trace) :: List.map symbol_list ~f:Bounds.NonNegativeBound.make_err_trace
-          |> Errlog.concat_traces )
-        curr_degree_with_term
+      ("", curr_cost_trace) :: polynomial_traces |> Errlog.concat_traces
     in
     let severity = Exceptions.Advice in
     Some
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index a76749bc7..57ce70391 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -999,7 +999,7 @@ module Bound = struct
         Symb.Symbol.exists_str ~f s
 end
 
-type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
+type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't
 
 module BoundTrace = struct
   type t =
@@ -1008,6 +1008,27 @@ module BoundTrace = struct
     | ModeledFunction of {pname: string; location: Location.t}
   [@@deriving compare]
 
+  let rec length = function
+    | Loop _ | ModeledFunction _ ->
+        1
+    | Call {callee_trace} ->
+        1 + length callee_trace
+
+
+  let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2)
+
+  let rec pp f = function
+    | Loop loc ->
+        F.fprintf f "Loop (%a)" Location.pp loc
+    | ModeledFunction {pname; location} ->
+        F.fprintf f "ModeledFunction `%s` (%a)" pname Location.pp location
+    | Call {callee_pname; callee_trace; location} ->
+        F.fprintf f "%a -> Call `%a` (%a)" pp callee_trace Typ.Procname.pp callee_pname Location.pp
+          location
+
+
+  let call ~callee_pname ~location callee_trace = Call {callee_pname; callee_trace; location}
+
   let make_err_trace =
     let rec aux depth trace =
       match trace with
@@ -1060,7 +1081,7 @@ module NonNegativeBound = struct
   let classify (b, trace) =
     match b with
     | Bound.PInf ->
-        ValTop
+        ValTop trace
     | Bound.MInf ->
         assert false
     | b -> (
@@ -1076,5 +1097,5 @@ module NonNegativeBound = struct
     | Bottom ->
         Constant NonNegativeInt.zero
     | NonBottom b ->
-        of_bound b ~trace:(BoundTrace.Call {callee_pname; location; callee_trace}) |> classify
+        of_bound b ~trace:(BoundTrace.call ~callee_pname ~location callee_trace) |> classify
 end
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index b298eca0d..4a4581f57 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -114,7 +114,15 @@ module Bound : sig
   val exists_str : f:(string -> bool) -> t -> bool
 end
 
-type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
+module BoundTrace : sig
+  include PrettyPrintable.PrintableOrderedType
+
+  val call : callee_pname:Typ.Procname.t -> location:Location.t -> t -> t
+
+  val make_err_trace : t -> Errlog.loc_trace
+end
+
+type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't
 
 module NonNegativeBound : sig
   type t [@@deriving compare]
@@ -133,8 +141,12 @@ module NonNegativeBound : sig
 
   val int_ub : t -> Ints.NonNegativeInt.t option
 
-  val classify : t -> (Ints.NonNegativeInt.t, t) valclass
+  val classify : t -> (Ints.NonNegativeInt.t, t, BoundTrace.t) valclass
 
   val subst :
-    Typ.Procname.t -> Location.t -> t -> Bound.eval_sym -> (Ints.NonNegativeInt.t, t) valclass
+       Typ.Procname.t
+    -> Location.t
+    -> t
+    -> Bound.eval_sym
+    -> (Ints.NonNegativeInt.t, t, BoundTrace.t) valclass
 end
diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml
index d94242297..b62b4431c 100644
--- a/infer/src/bufferoverrun/polynomials.ml
+++ b/infer/src/bufferoverrun/polynomials.ml
@@ -9,6 +9,7 @@ open! IStd
 open! AbstractDomain.Types
 module Bound = Bounds.Bound
 open Ints
+module TopTrace = Bounds.BoundTrace
 
 module DegreeKind = struct
   type t = Linear | Log [@@deriving compare]
@@ -56,14 +57,18 @@ end
 module type NonNegativeSymbol = sig
   type t [@@deriving compare]
 
-  val classify : t -> (Ints.NonNegativeInt.t, t) Bounds.valclass
+  val classify : t -> (Ints.NonNegativeInt.t, t, TopTrace.t) Bounds.valclass
 
   val int_lb : t -> NonNegativeInt.t
 
   val int_ub : t -> NonNegativeInt.t option
 
   val subst :
-    Typ.Procname.t -> Location.t -> t -> Bound.eval_sym -> (NonNegativeInt.t, t) Bounds.valclass
+       Typ.Procname.t
+    -> Location.t
+    -> t
+    -> Bound.eval_sym
+    -> (NonNegativeInt.t, t, TopTrace.t) Bounds.valclass
 
   val pp : F.formatter -> t -> unit
 end
@@ -92,8 +97,8 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
         Bounds.Constant (DegreeKind.compute degree_kind c)
     | Symbolic _ ->
         Bounds.Symbolic self
-    | ValTop ->
-        Bounds.ValTop
+    | ValTop trace ->
+        Bounds.ValTop trace
 
 
   let make degree_kind symbol = {degree_kind; symbol}
@@ -104,14 +109,14 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
     S.int_ub symbol |> Option.map ~f:(DegreeKind.compute degree_kind)
 
 
-  let subst callee_pname loc {degree_kind; symbol} eval =
-    match S.subst callee_pname loc symbol eval with
+  let subst callee_pname location {degree_kind; symbol} eval =
+    match S.subst callee_pname location symbol eval with
     | Constant c ->
         Bounds.Constant (DegreeKind.compute degree_kind c)
     | Symbolic symbol ->
         Bounds.Symbolic {degree_kind; symbol}
-    | ValTop ->
-        Bounds.ValTop
+    | ValTop trace ->
+        Bounds.ValTop trace
 
 
   let pp f {degree_kind; symbol} = DegreeKind.pp_hole S.pp f degree_kind symbol
@@ -198,13 +203,13 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
 
   let of_int_exn : int -> t = fun i -> i |> NonNegativeInt.of_int_exn |> of_non_negative_int
 
-  let of_valclass : (NonNegativeInt.t, S.t) Bounds.valclass -> t top_lifted = function
-    | ValTop ->
-        Top
+  let of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> (t, 't) below_above = function
+    | ValTop trace ->
+        Above trace
     | Constant i ->
-        NonTop (of_non_negative_int i)
+        Below (of_non_negative_int i)
     | Symbolic s ->
-        NonTop {const= NonNegativeInt.zero; terms= M.singleton s one}
+        Below {const= NonNegativeInt.zero; terms= M.singleton s one}
 
 
   let is_zero : t -> bool = fun {const; terms} -> NonNegativeInt.is_zero const && M.is_empty terms
@@ -311,13 +316,13 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
         if is_constant p1 then p1 else if is_constant p2 then p2 else p1
 
 
-  let subst callee_pname loc =
-    let exception ReturnTop in
+  let subst callee_pname location =
+    let exception ReturnTop of TopTrace.t in
     (* avoids top-lifting everything *)
     let rec subst {const; terms} eval_sym =
       M.fold
         (fun s p acc ->
-          match S.subst callee_pname loc s eval_sym with
+          match S.subst callee_pname location s eval_sym with
           | Constant c -> (
             match PositiveInt.of_big_int (c :> Z.t) with
             | None ->
@@ -325,15 +330,16 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
             | Some c ->
                 let p = subst p eval_sym in
                 mult_const_positive p c |> plus acc )
-          | ValTop ->
+          | ValTop trace ->
               let p = subst p eval_sym in
-              if is_zero p then acc else raise ReturnTop
+              if is_zero p then acc else raise (ReturnTop trace)
           | Symbolic s ->
               let p = subst p eval_sym in
               mult_symb p s |> plus acc )
         terms (of_non_negative_int const)
     in
-    fun p eval_sym -> match subst p eval_sym with p -> NonTop p | exception ReturnTop -> Top
+    fun p eval_sym ->
+      match subst p eval_sym with p -> Below p | exception ReturnTop trace -> Above trace
 
 
   (** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such degree *)
@@ -408,37 +414,64 @@ end
 module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
 module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind)
 
+module TopTraces = struct
+  include AbstractDomain.MinReprSet (TopTrace)
+
+  let make_err_trace traces =
+    match min_elt traces with None -> [] | Some trace -> TopTrace.make_err_trace trace
+end
+
 module NonNegativePolynomial = struct
-  type t = NonNegativeNonTopPolynomial.t top_lifted
+  (* Use Below for non-Top values and Above for Top values with their trace *)
+  type t = (NonNegativeNonTopPolynomial.t, TopTraces.t) below_above
 
-  let top = Top
+  type degree_with_term =
+    (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above
 
-  let ( <= ) = AbstractDomain.TopLiftedUtils.( <= ) ~le:NonNegativeNonTopPolynomial.( <= )
+  let ( <= ) =
+    AbstractDomain.StackedUtils.( <= ) ~le_below:NonNegativeNonTopPolynomial.( <= )
+      ~le_above:TopTraces.( <= )
+
+
+  let pp =
+    let pp_above f traces =
+      F.fprintf f "%t: %a" AbstractDomain.TopLiftedUtils.pp_top TopTraces.pp traces
+    in
+    AbstractDomain.StackedUtils.pp ~pp_below:NonNegativeNonTopPolynomial.pp ~pp_above
 
-  let pp = AbstractDomain.TopLiftedUtils.pp ~pp:NonNegativeNonTopPolynomial.pp
 
-  let zero = NonTop NonNegativeNonTopPolynomial.zero
+  let top = Above TopTraces.bottom
 
-  let one = NonTop NonNegativeNonTopPolynomial.one
+  let zero = Below NonNegativeNonTopPolynomial.zero
 
-  let of_int_exn i = NonTop (NonNegativeNonTopPolynomial.of_int_exn i)
+  let one = Below NonNegativeNonTopPolynomial.one
+
+  let of_int_exn i = Below (NonNegativeNonTopPolynomial.of_int_exn i)
+
+  let make_trace_set = AbstractDomain.StackedUtils.map ~f_below:Fn.id ~f_above:TopTraces.singleton
 
   let of_non_negative_bound ?(degree_kind = DegreeKind.Linear) b =
     b
     |> NonNegativeBoundWithDegreeKind.make degree_kind
     |> NonNegativeBoundWithDegreeKind.classify |> NonNegativeNonTopPolynomial.of_valclass
+    |> make_trace_set
+
 
+  let is_symbolic = function
+    | Above _ ->
+        false
+    | Below p ->
+        NonNegativeNonTopPolynomial.is_symbolic p
 
-  let is_symbolic = function Top -> false | NonTop p -> NonNegativeNonTopPolynomial.is_symbolic p
 
-  let is_top = function Top -> true | _ -> false
+  let is_top = function Above _ -> true | _ -> false
 
-  let is_zero = function NonTop p when NonNegativeNonTopPolynomial.is_zero p -> true | _ -> false
+  let is_zero = function Below p when NonNegativeNonTopPolynomial.is_zero p -> true | _ -> false
 
-  let is_one = function NonTop p when NonNegativeNonTopPolynomial.is_one p -> true | _ -> false
+  let is_one = function Below p when NonNegativeNonTopPolynomial.is_one p -> true | _ -> false
 
   let top_lifted_increasing ~f p1 p2 =
-    match (p1, p2) with Top, _ | _, Top -> Top | NonTop p1, NonTop p2 -> NonTop (f p1 p2)
+    AbstractDomain.StackedUtils.combine ~dir:`Increasing p1 p2 ~f_below:f ~f_above:TopTraces.join
 
 
   let plus = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.plus
@@ -446,54 +479,45 @@ module NonNegativePolynomial = struct
   let mult = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.mult
 
   let min_default_left p1 p2 =
-    match (p1, p2) with
-    | Top, x | x, Top ->
-        x
-    | NonTop p1, NonTop p2 ->
-        NonTop (NonNegativeNonTopPolynomial.min_default_left p1 p2)
+    AbstractDomain.StackedUtils.combine ~dir:`Decreasing p1 p2
+      ~f_below:NonNegativeNonTopPolynomial.min_default_left ~f_above:TopTraces.join
 
 
-  let subst callee_pname loc p eval_sym =
+  let subst callee_pname location p eval_sym =
     match p with
-    | Top ->
-        Top
-    | NonTop p ->
-        NonNegativeNonTopPolynomial.subst callee_pname loc p eval_sym
+    | Above callee_traces ->
+        Above
+          (TopTraces.map
+             (fun callee_trace -> TopTrace.call ~callee_pname ~location callee_trace)
+             callee_traces)
+    | Below p ->
+        NonNegativeNonTopPolynomial.subst callee_pname location p eval_sym |> make_trace_set
 
 
   let degree p =
-    match p with Top -> None | NonTop p -> Some (NonNegativeNonTopPolynomial.degree p)
-
-
-  let compare_by_degree p1 p2 =
-    match (p1, p2) with
-    | Top, Top ->
-        0
-    | Top, NonTop _ ->
-        1
-    | NonTop _, Top ->
-        -1
-    | NonTop p1, NonTop p2 ->
+    match p with Above _ -> None | Below p -> Some (NonNegativeNonTopPolynomial.degree p)
+
+
+  let compare_by_degree =
+    AbstractDomain.StackedUtils.compare ~cmp_above:TopTraces.compare ~cmp_below:(fun p1 p2 ->
         Degree.compare
           (NonNegativeNonTopPolynomial.degree p1)
-          (NonNegativeNonTopPolynomial.degree p2)
+          (NonNegativeNonTopPolynomial.degree p2) )
 
 
-  let get_degree_with_term = function
-    | Top ->
-        None
-    | NonTop p ->
-        Some (NonNegativeNonTopPolynomial.degree_with_term p)
+  let get_degree_with_term =
+    AbstractDomain.StackedUtils.map ~f_below:NonNegativeNonTopPolynomial.degree_with_term
+      ~f_above:Fn.id
 
 
-  let get_symbols p : Bounds.NonNegativeBound.t list =
-    match p with Top -> assert false | NonTop p -> NonNegativeNonTopPolynomial.get_symbols p
+  let get_symbols =
+    AbstractDomain.StackedUtils.map ~f_below:NonNegativeNonTopPolynomial.get_symbols ~f_above:Fn.id
 
 
   let pp_degree ~only_bigO fmt = function
-    | None ->
+    | Above _ ->
         Format.pp_print_string fmt "Top"
-    | Some (degree, degree_term) ->
+    | Below (degree, degree_term) ->
         if only_bigO then Format.fprintf fmt "O(%a)" NonNegativeNonTopPolynomial.pp degree_term
         else Degree.pp fmt degree
 
diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli
index 05484500d..ea702bb96 100644
--- a/infer/src/bufferoverrun/polynomials.mli
+++ b/infer/src/bufferoverrun/polynomials.mli
@@ -29,9 +29,18 @@ module NonNegativeNonTopPolynomial : sig
   val get_symbols : t -> Bounds.NonNegativeBound.t list
 end
 
+module TopTraces : sig
+  type t
+
+  val make_err_trace : t -> Errlog.loc_trace
+end
+
 module NonNegativePolynomial : sig
   include PrettyPrintable.PrintableType
 
+  type degree_with_term =
+    (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above
+
   val ( <= ) : lhs:t -> rhs:t -> bool
 
   val top : t
@@ -64,14 +73,14 @@ module NonNegativePolynomial : sig
 
   val compare_by_degree : t -> t -> int
 
-  val pp_degree :
-    only_bigO:bool -> Format.formatter -> (Degree.t * NonNegativeNonTopPolynomial.t) option -> unit
+  val pp_degree : only_bigO:bool -> Format.formatter -> degree_with_term -> unit
 
   val encode : t -> string
 
   val decode : string -> t
 
-  val get_symbols : t -> Bounds.NonNegativeBound.t list
+  val get_symbols :
+    t -> (Bounds.NonNegativeBound.t list, TopTraces.t) AbstractDomain.Types.below_above
 
-  val get_degree_with_term : t -> (Degree.t * NonNegativeNonTopPolynomial.t) option
+  val get_degree_with_term : t -> degree_with_term
 end
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index e4f8ecf59..1104fd746 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -685,6 +685,14 @@ module WorstCaseCost = struct
 end
 
 module Check = struct
+  let polynomial_traces cost =
+    match BasicCost.get_symbols cost with
+    | Below symbols ->
+        List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces
+    | Above trace ->
+        Polynomials.TopTraces.make_err_trace trace
+
+
   let report_threshold summary ~name ~location ~cost ~threshold =
     let degree_str =
       match BasicCost.degree cost with
@@ -703,12 +711,8 @@ module Check = struct
       let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
       Errlog.make_trace_element 0 location cost_desc []
     in
-    let full_trace =
-      BasicCost.get_symbols cost
-      |> List.map ~f:Bounds.NonNegativeBound.make_err_trace
-      |> Errlog.concat_traces
-    in
-    Reporting.log_error summary ~loc:location ~ltr:(cost_trace :: full_trace)
+    Reporting.log_error summary ~loc:location
+      ~ltr:(cost_trace :: polynomial_traces cost)
       ~extras:(compute_errlog_extras cost) IssueType.expensive_execution_time_call message
 
 
@@ -720,7 +724,8 @@ module Check = struct
           suffix
       in
       let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
-      Reporting.log_error ~loc ~extras:(compute_errlog_extras cost) summary issue message
+      Reporting.log_error ~loc ~ltr:(polynomial_traces cost) ~extras:(compute_errlog_extras cost)
+        summary issue message
     in
     if BasicCost.is_top cost then
       report IssueType.infinite_execution_time_call "cannot be computed"
diff --git a/infer/tests/build_systems/differential_of_costs_report/introduced.exp b/infer/tests/build_systems/differential_of_costs_report/introduced.exp
index ea5b3b079..54e38b351 100644
--- a/infer/tests/build_systems/differential_of_costs_report/introduced.exp
+++ b/infer/tests/build_systems/differential_of_costs_report/introduced.exp
@@ -1,3 +1,3 @@
-INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0, []
+INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0, [Loop at line 25]
 PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f4(int):int, 0, [Updated Cost is 6 + 5 ⋅ k (degree is 1),{k},Loop at line 44]
 PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f5(java.util.ArrayList):void, 0, [Updated Cost is 2 + list.length × log(list.length) (degree is 1 + 1⋅log),{list.length},Modeled call to List.length,{list.length},Modeled call to List.length]
diff --git a/infer/tests/codetoanalyze/c/performance/cost_test.c b/infer/tests/codetoanalyze/c/performance/cost_test.c
index 7ccad66b7..38cd8f15f 100644
--- a/infer/tests/codetoanalyze/c/performance/cost_test.c
+++ b/infer/tests/codetoanalyze/c/performance/cost_test.c
@@ -128,3 +128,21 @@ void call_while_upto20_10_good() { while_upto20_bad(10); }
 void call_while_upto20_unsigned_good(unsigned x) { while_upto20_bad(x); }
 
 void zero_cost_function() {}
+
+int always(int i) { return i % 2 == (i + 2) % 2; }
+
+void infinite_FN() {
+  int z;
+  for (int i = 0; always(i); i++) {
+    z += i;
+  }
+}
+
+void infinite() {
+  int z;
+  for (int i = 0; i % 2 == (i + 2) % 2; i++) {
+    z += i;
+  }
+}
+
+void call_infinite() { infinite(); }
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index 5e4332f20..adde1d33d 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -15,11 +15,15 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 43, column 3,{p},Loop at line 43, column 3]
-codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 63, column 3]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binary operation: ([-oo, +oo] + 1):signed32]
+codetoanalyze/c/performance/cost_test.c, call_infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [call to infinite,Loop at line 143, column 3]
 codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 726, degree = 0]
+codetoanalyze/c/performance/cost_test.c, infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 143, column 3]
+codetoanalyze/c/performance/cost_test.c, infinite, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32]
+codetoanalyze/c/performance/cost_test.c, infinite_FN, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32]
 codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1,{1+max(0, k)},Loop at line 85, column 3,{k},Loop at line 85, column 3]
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index bf613684d..04ae03885 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -4,7 +4,7 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void,
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset added: 5 Size: 4]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 53]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 1 Size: 0]
@@ -12,7 +12,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 2 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset: 1 Size: 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 164]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
@@ -36,13 +36,13 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(j
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, degree = 1,{p},Loop at line 12]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), degree = 2,{min(11, maxJ)},Loop at line 37,{min(11, maxI)},Loop at line 35,{12-max(0, maxJ)},Loop at line 35,{min(12, maxJ)},Loop at line 37,{maxI},Loop at line 35]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 31]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (x × x):signed32]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 17]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] × [0, +oo]):signed32]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 25]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.ensure_call(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 5 ⋅ list.length, degree = 1,{list.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (list.length - 1) + 5 ⋅ (list.length - 1) × list.length + 4 ⋅ list.length, degree = 2,{list.length},Loop at line 47,{list.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16,{list.length - 1},Loop at line 47]
@@ -57,7 +57,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 24]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
@@ -79,10 +79,10 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [0, 29]):signed32]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0]
-codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 15]
 codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, degree = 1,{test.a},Loop at line 16]
 codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58]
-codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 31]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32]
 codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 4 ⋅ (items.length + 1), degree = 1,{items.length + 1},Loop at line 66,{items.length},Loop at line 66]
@@ -105,7 +105,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length - 1), degree = 1,{length - 1},Loop at line 40]
 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 - 1) × (length - 1) + 8 ⋅ length, degree = 2,{length},Loop at line 50,{length - 1},Loop at line 51,{length - 1},Loop at line 50]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 30]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 20 + 33 ⋅ x.length, degree = 1,{x.length},Loop at line 73]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -115,7 +115,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ JSONArray.length().ub, degree = 1,{JSONArray.length().ub},Loop at line 18]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_quadratic(org.json.JSONArray):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ JSONArray.length().ub² + 4 ⋅ (1+max(0, JSONArray.length().ub)), degree = 2,{1+max(0, JSONArray.length().ub)},Loop at line 24,{JSONArray.length().ub},Loop at line 24,{JSONArray.length().ub},Loop at line 24]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 13 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},Loop at line 52]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 47]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1,{Math.min(...).ub + InputStream.read(...).ub},Loop at line 33]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62]