diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 732d177c7..84dc7adc2 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -1007,23 +1007,57 @@ type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
 
 (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *)
 module NonNegativeBound = struct
-  type t = Bound.t [@@deriving compare]
+  type trace =
+    | Loop of Location.t
+    | Call of {callee_pname: Typ.Procname.t; callee_trace: trace; location: Location.t}
+    | ModeledFunction of {pname: string; location: Location.t}
+  [@@deriving compare]
+
+  type t = Bound.t * trace [@@deriving compare]
+
+  let make_err_trace (b, t) =
+    let b = F.asprintf "{%a}" Bound.pp b in
+    let rec aux depth trace =
+      match trace with
+      | Loop loop_head_loc ->
+          let desc = F.asprintf "Loop at %a" Location.pp loop_head_loc in
+          [Errlog.make_trace_element depth loop_head_loc desc []]
+      | Call {callee_pname; location; callee_trace} ->
+          let desc = F.asprintf "call to %a" Typ.Procname.pp callee_pname in
+          Errlog.make_trace_element depth location desc [] :: aux (depth + 1) callee_trace
+      | ModeledFunction {pname; location} ->
+          let desc = F.asprintf "Modeled call to %s" pname in
+          [Errlog.make_trace_element depth location desc []]
+    in
+    (b, aux 0 t)
+
+
+  let pp fmt (bound, _) = Bound.pp fmt bound
+
+  let zero loop_head_loc = (Bound.zero, Loop loop_head_loc)
+
+  let check_le_zero b = if Bound.le b Bound.zero then Bound.zero else b
+
+  let of_bound ~trace b = (check_le_zero b, trace)
 
-  let pp = Bound.pp
+  let of_loop_bound loop_head_loc = of_bound ~trace:(Loop loop_head_loc)
 
-  let zero = Bound.zero
+  let of_modeled_function pname location b =
+    if Bound.lt b Bound.zero then (* we shouldn't have negative modeled bounds *)
+      assert false
+    else (b, ModeledFunction {pname; location})
 
-  let of_bound b = if Bound.le b zero then zero else b
 
-  let int_lb b =
+  let int_lb (b, _) =
     Bound.big_int_lb b
     |> Option.bind ~f:NonNegativeInt.of_big_int
     |> Option.value ~default:NonNegativeInt.zero
 
 
-  let int_ub b = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
+  let int_ub (b, _) = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
 
-  let classify = function
+  let classify (b, trace) =
+    match b with
     | Bound.PInf ->
         ValTop
     | Bound.MInf ->
@@ -1031,15 +1065,15 @@ module NonNegativeBound = struct
     | b -> (
       match Bound.is_const b with
       | None ->
-          Symbolic b
+          Symbolic (b, trace)
       | Some c ->
           Constant (NonNegativeInt.of_big_int_exn c) )
 
 
-  let subst b map =
+  let subst callee_pname location (b, callee_trace) map =
     match Bound.subst_ub b map with
     | Bottom ->
         Constant NonNegativeInt.zero
     | NonBottom b ->
-        of_bound b |> classify
+        of_bound b ~trace:(Call {callee_pname; location; callee_trace}) |> classify
 end
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index dba60155d..f01a2e422 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -127,13 +127,17 @@ end
 type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop
 
 module NonNegativeBound : sig
-  type t = Bound.t [@@deriving compare]
+  type t [@@deriving compare]
+
+  val of_loop_bound : Location.t -> Bound.t -> t
+
+  val of_modeled_function : string -> Location.t -> Bound.t -> t
 
   val pp : Format.formatter -> t -> unit
 
-  val zero : t
+  val make_err_trace : t -> string * Errlog.loc_trace
 
-  val of_bound : t -> t
+  val zero : Location.t -> t
 
   val int_lb : t -> Ints.NonNegativeInt.t
 
@@ -141,5 +145,6 @@ module NonNegativeBound : sig
 
   val classify : t -> (Ints.NonNegativeInt.t, t) valclass
 
-  val subst : t -> Bound.eval_sym -> (Ints.NonNegativeInt.t, t) valclass
+  val subst :
+    Typ.Procname.t -> Location.t -> t -> Bound.eval_sym -> (Ints.NonNegativeInt.t, t) valclass
 end
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 27c2e654b..b47f5b24c 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -17,6 +17,7 @@ module Relation = BufferOverrunDomainRelation
 module SPath = Symb.SymbolPath
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
+module LoopHeadLoc = Location
 
 type eval_sym_trace =
   { eval_sym: Bounds.Bound.eval_sym
@@ -547,14 +548,17 @@ module MemPure = struct
 
   let bot = empty
 
-  let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
+  let range :
+      filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t =
    fun ~filter_loc mem ->
     fold
       (fun loc v acc ->
-        if filter_loc loc then
-          v |> Val.get_itv |> Itv.range |> Itv.ItvRange.to_top_lifted_polynomial
-          |> Polynomials.NonNegativePolynomial.mult acc
-        else acc )
+        match filter_loc loc with
+        | Some loop_head_loc ->
+            v |> Val.get_itv |> Itv.range loop_head_loc |> Itv.ItvRange.to_top_lifted_polynomial
+            |> Polynomials.NonNegativePolynomial.mult acc
+        | None ->
+            acc )
       mem Polynomials.NonNegativePolynomial.one
 
 
@@ -1324,7 +1328,8 @@ module MemReach = struct
       add_from_locs m.mem_pure locs PowLoc.empty
 
 
-  let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
+  let range :
+      filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t =
    fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure
 
 
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index c587a21d4..050c201a6 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -18,13 +18,14 @@ module SymbolSet = Symb.SymbolSet
 module ItvRange = struct
   type t = Bounds.NonNegativeBound.t
 
-  let zero : t = Bounds.NonNegativeBound.zero
+  let zero loop_head : t = Bounds.NonNegativeBound.zero loop_head
 
-  let of_bounds : lb:Bound.t -> ub:Bound.t -> t =
-   fun ~lb ~ub ->
+  let of_bounds : loop_head_loc:Location.t -> lb:Bound.t -> ub:Bound.t -> t =
+   fun ~loop_head_loc ~lb ~ub ->
     Bound.plus_u ub Bound.one
     |> Bound.plus_u (Bound.neg lb)
-    |> Bound.simplify_bound_ends_from_paths |> Bounds.NonNegativeBound.of_bound
+    |> Bound.simplify_bound_ends_from_paths
+    |> Bounds.NonNegativeBound.of_loop_bound loop_head_loc
 
 
   let to_top_lifted_polynomial : t -> Polynomials.NonNegativePolynomial.t =
@@ -175,7 +176,9 @@ module ItvPure = struct
 
   let is_le_mone : t -> bool = fun (_, ub) -> Bound.le ub Bound.mone
 
-  let range : t -> ItvRange.t = fun (lb, ub) -> ItvRange.of_bounds ~lb ~ub
+  let range : Location.t -> t -> ItvRange.t =
+   fun loop_head_loc (lb, ub) -> ItvRange.of_bounds ~loop_head_loc ~lb ~ub
+
 
   let neg : t -> t =
    fun (l, u) ->
@@ -524,11 +527,11 @@ let le : lhs:t -> rhs:t -> bool = ( <= )
 
 let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x
 
-let range : t -> ItvRange.t = function
+let range loop_head : t -> ItvRange.t = function
   | Bottom ->
-      ItvRange.zero
+      ItvRange.zero loop_head
   | NonBottom itv ->
-      ItvPure.range itv
+      ItvPure.range loop_head itv
 
 
 let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t =
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 63f635634..8b65757a8 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -173,7 +173,7 @@ val le : lhs:t -> rhs:t -> bool
 
 val lnot : t -> Boolean.t
 
-val range : t -> ItvRange.t
+val range : Location.t -> t -> ItvRange.t
 
 val div : t -> t -> t
 
diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml
index b09730933..e38b893aa 100644
--- a/infer/src/bufferoverrun/polynomials.ml
+++ b/infer/src/bufferoverrun/polynomials.ml
@@ -62,7 +62,8 @@ module type NonNegativeSymbol = sig
 
   val int_ub : t -> NonNegativeInt.t option
 
-  val subst : t -> Bound.eval_sym -> (NonNegativeInt.t, t) Bounds.valclass
+  val subst :
+    Typ.Procname.t -> Location.t -> t -> Bound.eval_sym -> (NonNegativeInt.t, t) Bounds.valclass
 
   val pp : F.formatter -> t -> unit
 end
@@ -75,6 +76,8 @@ module type NonNegativeSymbolWithDegreeKind = sig
   val make : DegreeKind.t -> t0 -> t
 
   val degree_kind : t -> DegreeKind.t
+
+  val symbol : t -> t0
 end
 
 module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
@@ -101,8 +104,8 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
     S.int_ub symbol |> Option.map ~f:(DegreeKind.compute degree_kind)
 
 
-  let subst {degree_kind; symbol} eval =
-    match S.subst symbol eval with
+  let subst callee_pname loc {degree_kind; symbol} eval =
+    match S.subst callee_pname loc symbol eval with
     | Constant c ->
         Bounds.Constant (DegreeKind.compute degree_kind c)
     | Symbolic symbol ->
@@ -114,6 +117,8 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
   let pp f {degree_kind; symbol} = DegreeKind.pp_hole S.pp f degree_kind symbol
 
   let degree_kind {degree_kind} = degree_kind
+
+  let symbol {symbol} = symbol
 end
 
 module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
@@ -319,13 +324,13 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
    fun ~prev:_ ~next:_ ~num_iters:_ -> assert false
 
 
-  let subst =
+  let subst callee_pname loc =
     let exception ReturnTop in
     (* avoids top-lifting everything *)
     let rec subst {const; terms} eval_sym =
       M.fold
         (fun s p acc ->
-          match S.subst s eval_sym with
+          match S.subst callee_pname loc s eval_sym with
           | Constant c -> (
             match PositiveInt.of_big_int (c :> Z.t) with
             | None ->
@@ -406,6 +411,13 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
           terms const_not_zero
         : bool )
       |> ignore
+
+
+  let get_symbols p : S.t0 list =
+    let rec get_symbols_sub {terms} acc =
+      M.fold (fun s p acc -> get_symbols_sub p (S.symbol s :: acc)) terms acc
+    in
+    get_symbols_sub p []
 end
 
 module NonNegativePolynomial = struct
@@ -451,8 +463,12 @@ module NonNegativePolynomial = struct
 
   let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top
 
-  let subst p eval_sym =
-    match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p eval_sym
+  let subst callee_pname loc p eval_sym =
+    match p with
+    | Top ->
+        Top
+    | NonTop p ->
+        NonNegativeNonTopPolynomial.subst callee_pname loc p eval_sym
 
 
   let degree p =
@@ -490,6 +506,10 @@ module NonNegativePolynomial = struct
           (NonNegativeNonTopPolynomial.degree_term p)
 
 
+  let get_symbols p : Bounds.NonNegativeBound.t list =
+    match p with Top -> assert false | NonTop p -> NonNegativeNonTopPolynomial.get_symbols p
+
+
   let encode astate = Marshal.to_string astate [] |> Base64.encode_exn
 
   let decode enc_str = Marshal.from_string (Base64.decode_exn enc_str) 0
diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli
index dbc7726b2..1bb841a68 100644
--- a/infer/src/bufferoverrun/polynomials.mli
+++ b/infer/src/bufferoverrun/polynomials.mli
@@ -48,7 +48,7 @@ module NonNegativePolynomial : sig
 
   val min_default_left : t -> t -> t
 
-  val subst : t -> Bound.eval_sym -> t
+  val subst : Typ.Procname.t -> Location.t -> t -> Bound.eval_sym -> t
 
   val degree : t -> Degree.t option
 
@@ -61,4 +61,6 @@ module NonNegativePolynomial : sig
   val encode : t -> string
 
   val decode : string -> t
+
+  val get_symbols : t -> Bounds.NonNegativeBound.t list
 end
diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml
index e5faeb35b..348ca527d 100644
--- a/infer/src/checkers/control.ml
+++ b/infer/src/checkers/control.ml
@@ -21,7 +21,6 @@ module L = Logging
    3. remove invariant vars in the loop from control vars
  *)
 
-module VarSet = AbstractDomain.FiniteSet (Var)
 module CFG = ProcCfg.Normal
 module LoopHead = Procdesc.Node
 
@@ -35,6 +34,10 @@ module CVar = struct
 end
 
 module ControlDepSet = AbstractDomain.FiniteSet (CVar)
+
+(** Map control var -> loop head location  *)
+module ControlMap = PrettyPrintable.MakePPMap (Var)
+
 module GuardNodes = AbstractDomain.FiniteSet (Procdesc.Node)
 module LoopHeads = Procdesc.NodeSet
 
@@ -164,16 +167,17 @@ let remove_invariant_vars control_vars loop_inv_map =
     (fun {cvar; loop_head} acc ->
       match LoopInvariant.LoopHeadToInvVars.find_opt loop_head loop_inv_map with
       | Some inv_vars ->
-          if LoopInvariant.InvariantVars.mem cvar inv_vars then acc else VarSet.add cvar acc
+          if LoopInvariant.InvariantVars.mem cvar inv_vars then acc
+          else ControlMap.add cvar (Procdesc.Node.get_loc loop_head) acc
       | _ ->
           (* Each cvar is always attached to a loop head *)
           assert false )
-    control_vars VarSet.empty
+    control_vars ControlMap.empty
 
 
 let compute_control_vars control_invariant_map loop_inv_map node =
   let node_id = CFG.Node.id node in
-  let deps = VarSet.empty in
+  let deps = ControlMap.empty in
   ControlDepAnalyzer.extract_post node_id control_invariant_map
   |> Option.map ~f:(fun control_deps ->
          (* loop_inv_map: loop head -> variables that are invariant in the loop *)
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index 93a80f250..86ab91959 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -50,11 +50,11 @@ module BoundMap = struct
 
   let filter_loc vars_to_keep = function
     | AbsLoc.Loc.Var (Var.LogicalVar _) ->
-        false
-    | AbsLoc.Loc.Var var when Control.VarSet.mem var vars_to_keep ->
-        true
+        None
+    | AbsLoc.Loc.Var var ->
+        Control.ControlMap.find_opt var vars_to_keep
     | _ ->
-        false
+        None
 
 
   let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map loop_inv_map =
@@ -71,12 +71,13 @@ module BoundMap = struct
           match exit_state_opt with
           | Some entry_mem ->
               (* compute control vars, i.e. set of variables that affect the execution count *)
-              let control_vars =
+              let control_map =
                 Control.compute_control_vars control_invariant_map loop_inv_map node
               in
               L.(debug Analysis Medium)
                 "@\n>>> All dependencies for node = %a : %a  @\n\n" Procdesc.Node.pp node
-                Control.VarSet.pp control_vars ;
+                (Control.ControlMap.pp ~pp_value:Location.pp)
+                control_map ;
               (* bound = env(v1) *... * env(vn) *)
               let bound =
                 match entry_mem with
@@ -87,7 +88,7 @@ module BoundMap = struct
                        unreachable returning cost 0 \n" ;
                     BasicCost.zero
                 | NonBottom mem ->
-                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_vars) mem
+                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) mem
               in
               L.(debug Analysis Medium)
                 "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id BasicCost.pp
@@ -518,11 +519,12 @@ type extras_WCET =
   ; integer_type_widths: Typ.IntegerWidths.t
   ; get_node_nb_exec: Node.id -> BasicCost.t }
 
-let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_formals ~params ~callee_cost =
+let instantiate_cost integer_type_widths ~inferbo_caller_mem ~callee_pname ~callee_formals ~params
+    ~callee_cost ~loc =
   let eval_sym =
     BufferOverrunSemantics.mk_eval_sym integer_type_widths callee_formals params inferbo_caller_mem
   in
-  BasicCost.subst callee_cost eval_sym
+  BasicCost.subst callee_pname loc callee_cost eval_sym
 
 
 module InstrBasicCost = struct
@@ -531,12 +533,12 @@ module InstrBasicCost = struct
     For example for basic operation we set it to 1 and for function call we take it from the spec of the function.
   *)
 
-  let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_formals params
-      =
+  let callee_OperationCost callee_cost_record integer_type_widths inferbo_mem callee_pname
+      callee_formals params loc =
     let callee_cost = CostDomain.get_operation_cost callee_cost_record in
     if BasicCost.is_symbolic callee_cost then
-      instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_formals ~params
-        ~callee_cost
+      instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_pname
+        ~callee_formals ~params ~callee_cost ~loc
     else callee_cost
 
 
@@ -555,6 +557,7 @@ module InstrBasicCost = struct
   let get_instr_cost_record pdata instr_node instr =
     match instr with
     | Sil.Call (_, Exp.Const (Const.Cfun callee_pname), params, _, _) -> (
+        let loc = InstrCFG.Node.loc instr_node in
         let ProcData.({pdesc; extras= {inferbo_invariant_map; integer_type_widths}}) = pdata in
         match
           BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
@@ -564,13 +567,13 @@ module InstrBasicCost = struct
         | Some inferbo_mem -> (
           match CostModels.Call.dispatch () callee_pname params with
           | Some model ->
-              CostDomain.set_operation_cost (model inferbo_mem) CostDomain.zero_record
+              CostDomain.set_operation_cost (model loc inferbo_mem) CostDomain.zero_record
           | None -> (
             match get_callee_summary pdesc callee_pname with
             | Some ({CostDomain.post= callee_cost_record}, callee_formals) ->
                 let callee_operation_cost =
                   callee_OperationCost callee_cost_record integer_type_widths inferbo_mem
-                    callee_formals params
+                    callee_pname callee_formals params loc
                 in
                 let callee_allocation_cost = callee_AllocationCost callee_cost_record in
                 let callee_IO_cost = callee_IOCost callee_cost_record in
@@ -626,18 +629,23 @@ module WCET = struct
       | None ->
           ""
     in
-    let ltr =
-      let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
-      [Errlog.make_trace_element 0 loc cost_desc []]
-    in
     let message =
       F.asprintf
         "The execution time from the beginning of the function up to this program point is likely \
          above the acceptable threshold of %a (estimated cost %a%s)"
         BasicCost.pp expensive_threshold BasicCost.pp cost degree_str
     in
-    Reporting.log_error summary ~loc ~ltr ~extras:(compute_errlog_extras cost)
-      IssueType.expensive_execution_time_call message
+    let cost_trace =
+      let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
+      Errlog.make_trace_element 0 loc 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 ~ltr:(cost_trace :: full_trace)
+      ~extras:(compute_errlog_extras cost) IssueType.expensive_execution_time_call message
 
 
   (*
diff --git a/infer/src/checkers/cost.mli b/infer/src/checkers/cost.mli
index 26975dab2..2d778b621 100644
--- a/infer/src/checkers/cost.mli
+++ b/infer/src/checkers/cost.mli
@@ -12,7 +12,9 @@ val checker : Callbacks.proc_callback_t
 val instantiate_cost :
      Typ.IntegerWidths.t
   -> inferbo_caller_mem:BufferOverrunDomain.Mem.t
+  -> callee_pname:Typ.Procname.t
   -> callee_formals:(Pvar.t * Typ.t) list
   -> params:(Exp.t * 'a) list
   -> callee_cost:CostDomain.BasicCost.t
+  -> loc:Location.t
   -> CostDomain.BasicCost.t
diff --git a/infer/src/checkers/costModels.ml b/infer/src/checkers/costModels.ml
index 3334bf62d..c8d1acad4 100644
--- a/infer/src/checkers/costModels.ml
+++ b/infer/src/checkers/costModels.ml
@@ -8,10 +8,10 @@
 open! IStd
 module BasicCost = CostDomain.BasicCost
 
-type model = BufferOverrunDomain.Mem.t -> BasicCost.t
+type model = Location.t -> BufferOverrunDomain.Mem.t -> BasicCost.t
 
 module Collections = struct
-  let eval_collection_length coll_exp inferbo_mem =
+  let eval_collection_length coll_exp loc inferbo_mem =
     let upper_bound =
       let itv =
         BufferOverrunModels.Collection.eval_collection_length coll_exp inferbo_mem
@@ -19,7 +19,7 @@ module Collections = struct
       in
       match itv with Bottom -> Bounds.Bound.PInf | NonBottom itv_pure -> Itv.ItvPure.ub itv_pure
     in
-    Bounds.NonNegativeBound.of_bound upper_bound
+    Bounds.NonNegativeBound.of_modeled_function "List.length" loc upper_bound
 
 
   let n_log_n b =
@@ -28,8 +28,8 @@ module Collections = struct
     BasicCost.mult n log_n
 
 
-  let sort coll_exp inferbo_mem =
-    let length = eval_collection_length coll_exp inferbo_mem in
+  let sort coll_exp loc inferbo_mem =
+    let length = eval_collection_length coll_exp loc inferbo_mem in
     n_log_n length
 end
 
diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml
index bee75c557..63f83ba82 100644
--- a/infer/src/checkers/hoisting.ml
+++ b/infer/src/checkers/hoisting.ml
@@ -93,16 +93,19 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in
     match Ondemand.analyze_proc_name pname with
     | Some ({Summary.payloads= {Payloads.cost= Some {CostDomain.post= cost_record}}} as summary)
       when CostDomain.BasicCost.is_symbolic (CostDomain.get_operation_cost cost_record) ->
-        let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in
+        let last_node = InstrCFG.last_of_underlying_node node in
+        let instr_node_id = InstrCFG.Node.id last_node in
         let inferbo_invariant_map = Lazy.force inferbo_invariant_map in
         let inferbo_mem =
           Option.value_exn (BufferOverrunAnalysis.extract_pre instr_node_id inferbo_invariant_map)
         in
         let callee_formals = Summary.get_proc_desc summary |> Procdesc.get_pvar_formals in
+        let loc = InstrCFG.Node.loc last_node in
         (* get the cost of the function call *)
-        Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem ~callee_formals
-          ~params
+        Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem
+          ~callee_pname:pname ~callee_formals ~params
           ~callee_cost:(CostDomain.get_operation_cost cost_record)
+          ~loc
         |> CostDomain.BasicCost.is_symbolic
     | _ ->
         false
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index 85cd46e6e..6e994047a 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -1,8 +1,8 @@
-codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},call to break_loop,Loop at line 10, column 3,{p},call to break_loop,Loop at line 10, column 3]
+codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 10, column 3,{p},Loop at line 10, column 3]
+codetoanalyze/c/performance/break.c, break_loop_with_t, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 22, column 3,{p},Loop at line 22, column 3]
 codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 13, column 3,{m},Loop at line 13, column 3]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/compound_loop_guard.c, nested_while_and_or, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
@@ -14,7 +14,7 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 8, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 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]
+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, 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]
@@ -22,9 +22,9 @@ codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bu
 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, 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]
+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]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 214, degree = 0]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m + 20), degree = 1,{-m + 20},Loop at line 117, column 3]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1307, degree = 0]
@@ -44,13 +44,13 @@ codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 12, EXPENSIVE_EXE
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([3, +oo] + 1):signed32]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 551, degree = 0]
 codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16007, degree = 0]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m - 1) × m + 8 ⋅ m + 2 ⋅ m × (max(1, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m + 6 ⋅ m² + 2 ⋅ m × (1+max(0, m)) + 2 ⋅ (1+max(0, m)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m - 1) × m + 8 ⋅ m + 2 ⋅ m × (max(1, m)) + 2 ⋅ (1+max(0, m)), degree = 2,{1+max(0, m)},Loop at line 31, column 3,{max(1, m)},call to do_n_times,Loop at line 12, column 3,{m},Loop at line 31, column 3,{m},Loop at line 31, column 3,{m - 1},call to do_n_times,Loop at line 12, column 3]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m + 6 ⋅ m × m + 2 ⋅ m × (1+max(0, m)) + 2 ⋅ (1+max(0, m)), degree = 2,{1+max(0, m)},Loop at line 24, column 3,{1+max(0, m)},call to do_n_times,Loop at line 12, column 3,{m},call to do_n_times,Loop at line 12, column 3,{m},Loop at line 24, column 3]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1,{1+max(0, n)},Loop at line 12, column 3,{n},Loop at line 12, column 3]
+codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1,{1+max(0, n)},Loop at line 23, column 3,{n},Loop at line 23, column 3]
+codetoanalyze/c/performance/invariant.c, do_k_times_array, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), degree = 1,{1+max(0, n)},Loop at line 31, column 3,{n},Loop at line 31, column 3]
+codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n + 3 ⋅ n × m + 2 ⋅ n × (1+max(0, m)) + 2 ⋅ (1+max(0, n)), degree = 2,{1+max(0, n)},Loop at line 40, column 3,{1+max(0, m)},Loop at line 41, column 5,{m},Loop at line 41, column 5,{n},Loop at line 40, column 3]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 50, column 3,{p},Loop at line 50, column 3]
 codetoanalyze/c/performance/invariant.c, while_infinite_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004, degree = 0]
 codetoanalyze/c/performance/loops.c, do_while_independent_of_p, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 227, degree = 0]
@@ -58,12 +58,12 @@ codetoanalyze/c/performance/loops.c, if_in_loop, 3, EXPENSIVE_EXECUTION_TIME_CAL
 codetoanalyze/c/performance/loops.c, if_in_loop, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/loops.c, if_out_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 615, degree = 0]
 codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
-codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1]
+codetoanalyze/c/performance/loops.c, loop_use_global_vars, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1,{1+max(0, x)},Loop at line 69, column 3,{x},Loop at line 69, column 3]
 codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
 codetoanalyze/c/performance/switch_continue.c, test_switch, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/performance/switch_continue.c, test_switch, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 602, degree = 0]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 25 + 12 ⋅ (n - 1), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/switch_continue.c, unroll_loop, 14, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 25 + 12 ⋅ (n - 1), degree = 1,{n - 1},Loop at line 43, column 11]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 13, column 3,{m},Loop at line 13, column 3]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 25, column 3,{m},Loop at line 25, column 3]
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index a16e22b79..3b1a814e0 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -1,6 +1,6 @@
 codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_overrun_bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [2, 8] Size: 8]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length, degree = 1]
-codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ mag.length, degree = 1]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length, degree = 1,{length},Loop at line 28]
+codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ mag.length, degree = 1,{mag.length},Loop at line 15]
 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]
@@ -18,20 +18,20 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov
 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]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_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.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to List.length,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to List.length]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 14]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2,{-Integer.intValue().lb + 11},Loop at line 193,{list.length},Loop at line 193,{-Integer.intValue().lb + 11},Loop at line 193,{list.length - 1},Loop at line 193]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 ⋅ (list1.length - 1) + 4 ⋅ list1.length, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ list.length, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 13 ⋅ (list1.length - 1) + 4 ⋅ list1.length, degree = 1,{list1.length},Loop at line 184,{list1.length - 1},Loop at line 184]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 19]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1,{list.length},Loop at line 176,{list.length - 1},Loop at line 176]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1,{list.length},Loop at line 170,{list.length - 1},Loop at line 170]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 14 ⋅ (this.list.length - 1) + 4 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 216,{this.list.length - 1},Loop at line 216]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log]
-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]
-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]
-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]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},Modeled call to List.length,{list.length},Modeled call to List.length]
+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, 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>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
@@ -40,15 +40,15 @@ codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):v
 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, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,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]
-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]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size + 5 ⋅ size × list.length, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 10 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3]
+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]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 16]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1,{mSubscribers.length},Loop at line 28,{mSubscribers.length - 1},Loop at line 28]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.length, degree = 1,{mSubscribers.length},Loop at line 21,{mSubscribers.length - 1},Loop at line 21]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size + 5 ⋅ size × list.length, degree = 2,{list.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16,{size},Loop at line 40]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length - 1) + 33 ⋅ (list1.length - 1) × (list2.length - 1) + 5 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 5 ⋅ (list1.length - 1) × (list2.length - 1) × list1.length + 4 ⋅ (list1.length - 1) × list2.length + 4 ⋅ list1.length, degree = 3,{list1.length},Loop at line 54,{list2.length},Loop at line 55,{list1.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16,{list1.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16,{list2.length - 1},Loop at line 55,{list1.length - 1},Loop at line 54]
 codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1,{1+max(0, m)},Loop at line 15,{m},Loop at line 15]
 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, 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]
@@ -57,7 +57,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc
 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]
-codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, degree = 1]
+codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, degree = 1,{k},Loop at line 90]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202, degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1303, degree = 0]
 codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop3(int):int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 237, degree = 0]
@@ -76,43 +76,43 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 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/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]
-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]
+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, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `size`,<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>,Assignment,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]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size + 20), degree = 1]
-codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length - 1) + 4 ⋅ parts.length, degree = 1]
-codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 87 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 44 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 38 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
-codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 28 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
+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]
+codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2,{5+min(0, size)},Loop at line 46,{5+min(1, size)},Loop at line 46,{size + 5},Loop at line 46]
+codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ (size + 20), degree = 1,{size + 20},Loop at line 19]
+codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length - 1) + 4 ⋅ parts.length, degree = 1,{parts.length},Loop at line 12,{parts.length - 1},Loop at line 12]
+codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 87 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonMap.addKeyToMap(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 44 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to StringBuilder JsonUtils.serialize(String),call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},Loop at line 13]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 38 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.serialize(StringBuilder,String),call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
+codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 28 + 74 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void JsonUtils.escape(StringBuilder,String),Loop at line 13]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
-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]
-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)² + 8 ⋅ length, degree = 2]
+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, 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]
+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]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 13 ⋅ String.toCharArray().length.ub, degree = 1]
-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]
-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]
-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]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 13 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},call to void UnknownCallsTest.loop_over_charArray(StringBuilder,String),Loop at line 52]
+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, 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]
-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]
+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]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]]