diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml
index 23ed09cad..78fe74de0 100644
--- a/infer/src/base/IssueType.ml
+++ b/infer/src/base/IssueType.ml
@@ -89,6 +89,8 @@ module Unsafe : sig
   val all_issues : unit -> t list
 
   val set_enabled : t -> bool -> unit
+
+  module IssueSet : PrettyPrintable.PPUniqRankSet with type elt = t
 end = struct
   module T = struct
     type t =
@@ -978,10 +980,18 @@ let wrong_argument_number =
 let unreachable_cost_call ~kind = register_cost ~enabled:false ~kind "%s_UNREACHABLE_AT_EXIT"
 
 (* register enabled cost issues *)
-let () =
+let is_autoreleasepool_size_issue =
+  let autoreleasepool_size_issues = ref IssueSet.empty in
+  let add_autoreleasepool_size_issue ~kind issue_type =
+    match (kind : CostKind.t) with
+    | AutoreleasepoolSize ->
+        autoreleasepool_size_issues := IssueSet.add !autoreleasepool_size_issues issue_type
+    | OperationCost | AllocationCost ->
+        ()
+  in
   List.iter CostKind.enabled_cost_kinds ~f:(fun CostKind.{kind} ->
       List.iter [true; false] ~f:(fun is_on_ui_thread ->
-          ignore (unreachable_cost_call ~kind) ;
-          ignore (infinite_cost_call ~kind) ;
-          ignore (complexity_increase ~kind ~is_on_ui_thread) ;
-          () ) )
+          add_autoreleasepool_size_issue ~kind (unreachable_cost_call ~kind) ;
+          add_autoreleasepool_size_issue ~kind (infinite_cost_call ~kind) ;
+          add_autoreleasepool_size_issue ~kind (complexity_increase ~kind ~is_on_ui_thread) ) ) ;
+  fun issue_type -> IssueSet.mem issue_type !autoreleasepool_size_issues
diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli
index a3c7dc1f2..df485b13a 100644
--- a/infer/src/base/IssueType.mli
+++ b/infer/src/base/IssueType.mli
@@ -351,3 +351,5 @@ val weak_self_in_noescape_block : t
 val wrong_argument_number : t
 
 val unreachable_cost_call : kind:CostKind.t -> t
+
+val is_autoreleasepool_size_issue : t -> bool
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 1c2b6ce58..69a5c8dec 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -1294,6 +1294,8 @@ module BoundTrace = struct
 
 
   let of_loop location = Loop location
+
+  let of_modeled_function pname location = ModeledFunction {pname; location}
 end
 
 (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index 88021ca07..96067ce97 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -145,7 +145,11 @@ module BoundTrace : sig
 
   val make_err_trace : depth:int -> t -> Errlog.loc_trace
 
+  val call : callee_pname:Procname.t -> location:Location.t -> t -> t
+
   val of_loop : Location.t -> t
+
+  val of_modeled_function : string -> Location.t -> t
 end
 
 type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index fdd0dc3b1..3d755f98c 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -777,7 +777,8 @@ module MemPure = struct
                 acc )
         | None ->
             acc )
-      mem Polynomials.NonNegativePolynomial.one
+      mem
+      (Polynomials.NonNegativePolynomial.one ())
 
 
   let join oenv astate1 astate2 =
diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml
index 9e7731b90..45335ef0d 100644
--- a/infer/src/bufferoverrun/polynomials.ml
+++ b/infer/src/bufferoverrun/polynomials.ml
@@ -72,6 +72,8 @@ module type NonNegativeSymbol = sig
   val pp : hum:bool -> F.formatter -> t -> unit
 
   val split_mult : t -> (t * t) option
+
+  val make_err_trace : t -> string * Errlog.loc_trace
 end
 
 module type NonNegativeSymbolWithDegreeKind = sig
@@ -86,6 +88,8 @@ module type NonNegativeSymbolWithDegreeKind = sig
   val symbol : t -> t0
 
   val split_mult : t -> (t * t) option
+
+  val make_err_trace_symbol : t0 -> string * Errlog.loc_trace
 end
 
 module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
@@ -135,6 +139,11 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
 
   let split_mult {degree_kind; symbol} =
     Option.map (S.split_mult symbol) ~f:(fun (s1, s2) -> (make degree_kind s1, make degree_kind s2))
+
+
+  let make_err_trace {symbol} = S.make_err_trace symbol
+
+  let make_err_trace_symbol symbol = S.make_err_trace symbol
 end
 
 module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
@@ -207,47 +216,83 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
       - symbols children of a term are 'smaller' than its self symbol
       - contents of terms are not zero
       - symbols in terms are only symbolic values *)
-  type t = {const: NonNegativeInt.t; terms: t M.t} [@@deriving compare]
+  type poly = {const: NonNegativeInt.t; terms: poly M.t} [@@deriving compare]
+
+  type t = {poly: poly; autoreleasepool_trace: Bounds.BoundTrace.t option} [@@deriving compare]
+
+  let get_autoreleasepool_trace {autoreleasepool_trace} = autoreleasepool_trace
+
+  let join_autoreleasepool_trace x y = Option.first_some x y
+
+  let poly_of_non_negative_int : NonNegativeInt.t -> poly = fun const -> {const; terms= M.empty}
+
+  let of_non_negative_int : ?autoreleasepool_trace:Bounds.BoundTrace.t -> NonNegativeInt.t -> t =
+   fun ?autoreleasepool_trace const -> {poly= poly_of_non_negative_int const; autoreleasepool_trace}
+
 
-  let of_non_negative_int : NonNegativeInt.t -> t = fun const -> {const; terms= M.empty}
+  let zero_poly = poly_of_non_negative_int NonNegativeInt.zero
 
   let zero = of_non_negative_int NonNegativeInt.zero
 
-  let one = of_non_negative_int NonNegativeInt.one
+  let one_poly = poly_of_non_negative_int NonNegativeInt.one
 
-  let of_int_exn : int -> t = fun i -> i |> NonNegativeInt.of_int_exn |> of_non_negative_int
+  let one ?autoreleasepool_trace () = of_non_negative_int ?autoreleasepool_trace NonNegativeInt.one
 
-  let is_zero : t -> bool = fun {const; terms} -> NonNegativeInt.is_zero const && M.is_empty terms
+  let of_int_exn : ?autoreleasepool_trace:Bounds.BoundTrace.t -> int -> t =
+   fun ?autoreleasepool_trace i ->
+    i |> NonNegativeInt.of_int_exn |> of_non_negative_int ?autoreleasepool_trace
 
-  let is_one : t -> bool = fun {const; terms} -> NonNegativeInt.is_one const && M.is_empty terms
 
-  let is_constant : t -> bool = fun {terms} -> M.is_empty terms
+  let is_zero_poly : poly -> bool =
+   fun {const; terms} -> NonNegativeInt.is_zero const && M.is_empty terms
+
+
+  let is_zero : t -> bool = fun {poly} -> is_zero_poly poly
+
+  let is_one_poly : poly -> bool =
+   fun {const; terms} -> NonNegativeInt.is_one const && M.is_empty terms
+
+
+  let is_one : t -> bool = fun {poly} -> is_one_poly poly
+
+  let is_constant : t -> bool = fun {poly= {terms}} -> M.is_empty terms
 
   let is_symbolic : t -> bool = fun p -> not (is_constant p)
 
-  let rec plus : t -> t -> t =
+  let rec plus_poly : poly -> poly -> poly =
    fun p1 p2 ->
     { const= NonNegativeInt.(p1.const + p2.const)
-    ; terms= M.increasing_union ~f:plus p1.terms p2.terms }
+    ; terms= M.increasing_union ~f:plus_poly p1.terms p2.terms }
+
 
+  let plus : t -> t -> t =
+   fun p1 p2 ->
+    { poly= plus_poly p1.poly p2.poly
+    ; autoreleasepool_trace=
+        join_autoreleasepool_trace p1.autoreleasepool_trace p2.autoreleasepool_trace }
 
-  let rec mult_const_positive : t -> PositiveInt.t -> t =
+
+  let rec mult_const_positive : poly -> PositiveInt.t -> poly =
    fun {const; terms} c ->
     { const= NonNegativeInt.(const * (c :> NonNegativeInt.t))
     ; terms= M.map (fun p -> mult_const_positive p c) terms }
 
 
-  let mult_const : t -> NonNegativeInt.t -> t =
+  let mult_const_poly : poly -> NonNegativeInt.t -> poly =
    fun p c ->
-    match PositiveInt.of_big_int (c :> Z.t) with None -> zero | Some c -> mult_const_positive p c
+    match PositiveInt.of_big_int (c :> Z.t) with
+    | None ->
+        zero_poly
+    | Some c ->
+        mult_const_positive p c
 
 
   (* (c + r * R + s * S + t * T) x s
      = 0 + r * (R x s) + s * (c + s * S + t * T) *)
-  let rec mult_symb : t -> S.t -> t =
+  let rec mult_symb_poly : poly -> S.t -> poly =
    fun {const; terms} s ->
     let less_than_s, equal_s_opt, greater_than_s = M.split s terms in
-    let less_than_s = M.map (fun p -> mult_symb p s) less_than_s in
+    let less_than_s = M.map (fun p -> mult_symb_poly p s) less_than_s in
     let s_term =
       let terms =
         match equal_s_opt with
@@ -258,17 +303,30 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
       in
       {const; terms}
     in
-    let terms = if is_zero s_term then less_than_s else M.add s s_term less_than_s in
+    let terms = if is_zero_poly s_term then less_than_s else M.add s s_term less_than_s in
     {const= NonNegativeInt.zero; terms}
 
 
-  let rec mult : t -> t -> t =
+  let mult_symb : t -> S.t -> t = fun x s -> {x with poly= mult_symb_poly x.poly s}
+
+  let rec mult_poly : poly -> poly -> poly =
    fun p1 p2 ->
-    if is_zero p1 || is_zero p2 then zero
-    else if is_one p1 then p2
-    else if is_one p2 then p1
+    if is_zero_poly p1 || is_zero_poly p2 then zero_poly
+    else if is_one_poly p1 then p2
+    else if is_one_poly p2 then p1
     else
-      mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms
+      mult_const_poly p1 p2.const
+      |> M.fold (fun s p acc -> plus_poly (mult_symb_poly (mult_poly p p1) s) acc) p2.terms
+
+
+  let mult : t -> t -> t =
+   fun p1 p2 ->
+    let poly = mult_poly p1.poly p2.poly in
+    let autoreleasepool_trace =
+      if is_zero_poly poly then None
+      else join_autoreleasepool_trace p1.autoreleasepool_trace p2.autoreleasepool_trace
+    in
+    {poly; autoreleasepool_trace}
 
 
   let rec of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> ('t, t, 't) below_above =
@@ -280,7 +338,9 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
     | Symbolic s -> (
       match S.split_mult s with
       | None ->
-          Val {const= NonNegativeInt.zero; terms= M.singleton s one}
+          Val
+            { poly= {const= NonNegativeInt.zero; terms= M.singleton s one_poly}
+            ; autoreleasepool_trace= None }
       | Some (s1, s2) -> (
         match (of_valclass (S.classify s1), of_valclass (S.classify s2)) with
         | Val s1, Val s2 ->
@@ -311,34 +371,42 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
 
 
   (* assumes symbols are not comparable *)
-  let rec leq : lhs:t -> rhs:t -> bool =
+  let rec leq_poly : lhs:poly -> rhs:poly -> bool =
    fun ~lhs ~rhs ->
     phys_equal lhs rhs
-    || (NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:leq lhs.terms rhs.terms)
+    || NonNegativeInt.leq ~lhs:lhs.const ~rhs:rhs.const
+       && M.le ~le_elt:leq_poly lhs.terms rhs.terms
     || Option.exists (int_ub lhs) ~f:(fun lhs_ub ->
            NonNegativeInt.leq ~lhs:lhs_ub ~rhs:(int_lb rhs) )
 
 
-  let rec xcompare ~lhs ~rhs =
+  let leq ~lhs ~rhs = leq_poly ~lhs:lhs.poly ~rhs:rhs.poly
+
+  let rec xcompare_poly ~lhs ~rhs =
     let cmp_const =
       PartialOrder.of_compare ~compare:NonNegativeInt.compare ~lhs:lhs.const ~rhs:rhs.const
     in
-    let cmp_terms = M.xcompare ~xcompare_elt:xcompare ~lhs:lhs.terms ~rhs:rhs.terms in
+    let cmp_terms = M.xcompare ~xcompare_elt:xcompare_poly ~lhs:lhs.terms ~rhs:rhs.terms in
     PartialOrder.join cmp_const cmp_terms
 
 
-  let rec mask_min_max_constant {const; terms} =
+  let xcompare ~lhs ~rhs = xcompare_poly ~lhs:lhs.poly ~rhs:rhs.poly
+
+  let rec mask_min_max_constant_poly {const; terms} =
     { const
     ; terms=
         M.fold
           (fun s p acc ->
-            let p' = mask_min_max_constant p in
+            let p' = mask_min_max_constant_poly p in
             M.update (S.mask_min_max_constant s)
-              (function None -> Some p' | Some p -> if leq ~lhs:p ~rhs:p' then Some p' else Some p)
+              (function
+                | None -> Some p' | Some p -> if leq_poly ~lhs:p ~rhs:p' then Some p' else Some p )
               acc )
           terms M.empty }
 
 
+  let mask_min_max_constant x = {x with poly= mask_min_max_constant_poly x.poly}
+
   (* assumes symbols are not comparable *)
   (* TODO: improve this for comparable symbols *)
   let min_default_left : t -> t -> t =
@@ -355,7 +423,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
   let subst callee_pname location =
     let exception ReturnTop of (S.t * Bounds.BoundTrace.t) in
     (* avoids top-lifting everything *)
-    let rec subst {const; terms} eval_sym =
+    let rec subst_poly {const; terms} eval_sym =
       M.fold
         (fun s p acc ->
           match S.subst callee_pname location s eval_sym with
@@ -364,36 +432,48 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
             | None ->
                 acc
             | Some c ->
-                let p = subst p eval_sym in
-                mult_const_positive p c |> plus acc )
+                let p = subst_poly p eval_sym in
+                mult_const_positive p c |> plus_poly acc )
           | ValTop trace ->
-              let p = subst p eval_sym in
-              if is_zero p then acc else raise (ReturnTop (s, trace))
+              let p = subst_poly p eval_sym in
+              if is_zero_poly p then acc else raise (ReturnTop (s, trace))
           | Symbolic s ->
-              let p = subst p eval_sym in
-              mult_symb p s |> plus acc )
-        terms (of_non_negative_int const)
+              let p = subst_poly p eval_sym in
+              mult_symb_poly p s |> plus_poly acc )
+        terms (poly_of_non_negative_int const)
     in
-    fun p eval_sym ->
-      match subst p eval_sym with p -> Val p | exception ReturnTop s_trace -> Above s_trace
+    fun {poly; autoreleasepool_trace} eval_sym ->
+      match subst_poly poly eval_sym with
+      | poly ->
+          let autoreleasepool_trace =
+            Option.map autoreleasepool_trace ~f:(fun autoreleasepool_trace ->
+                Bounds.BoundTrace.call ~callee_pname ~location autoreleasepool_trace )
+          in
+          Val {poly; autoreleasepool_trace}
+      | exception ReturnTop s_trace ->
+          Above s_trace
 
 
   (** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such
       degree *)
-  let rec degree_with_term {terms} =
-    M.fold
-      (fun t p cur_max ->
-        let d, p' = degree_with_term p in
-        let degree_term = (Degree.succ (S.degree_kind t) d, mult_symb p' t) in
-        if [%compare: Degree.t * t] degree_term cur_max > 0 then degree_term else cur_max )
-      terms (Degree.zero, one)
+  let degree_with_term {poly; autoreleasepool_trace} =
+    let rec degree_with_term_poly {terms} =
+      M.fold
+        (fun t p cur_max ->
+          let d, p' = degree_with_term_poly p in
+          let degree_term = (Degree.succ (S.degree_kind t) d, mult_symb p' t) in
+          if [%compare: Degree.t * t] degree_term cur_max > 0 then degree_term else cur_max )
+        terms
+        (Degree.zero, one ?autoreleasepool_trace ())
+    in
+    degree_with_term_poly poly
 
 
   let degree p = fst (degree_with_term p)
 
   let multiplication_sep = F.sprintf " %s " SpecialChars.multiplication_sign
 
-  let pp : hum:bool -> F.formatter -> t -> unit =
+  let pp_poly : hum:bool -> F.formatter -> poly -> unit =
     let add_symb s (((last_s, last_occ) as last), others) =
       if Int.equal 0 (S.compare s last_s) then ((last_s, PositiveInt.succ last_occ), others)
       else ((s, PositiveInt.one), last :: others)
@@ -442,11 +522,22 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
       |> ignore
 
 
+  let pp : hum:bool -> F.formatter -> t -> unit = fun ~hum fmt {poly} -> pp_poly ~hum fmt poly
+
   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 []
+    get_symbols_sub p.poly []
+
+
+  let polynomial_traces ?(is_autoreleasepool_trace = false) p =
+    let traces = get_symbols p |> List.map ~f:S.make_err_trace_symbol in
+    if is_autoreleasepool_trace then
+      get_autoreleasepool_trace p
+      |> Option.value_map ~default:traces ~f:(fun trace ->
+             traces @ [("autorelease", Bounds.BoundTrace.make_err_trace ~depth:0 trace)] )
+    else traces
 end
 
 module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound)
@@ -594,13 +685,17 @@ module NonNegativePolynomial = struct
 
   let zero = Val NonNegativeNonTopPolynomial.zero
 
-  let one = Val NonNegativeNonTopPolynomial.one
+  let one ?autoreleasepool_trace () =
+    Val (NonNegativeNonTopPolynomial.one ?autoreleasepool_trace ())
+
 
   let of_unreachable node_loc =
     Below (UnreachableTraces.singleton (UnreachableTrace.unreachable_node node_loc))
 
 
-  let of_int_exn i = Val (NonNegativeNonTopPolynomial.of_int_exn i)
+  let of_int_exn ?autoreleasepool_trace i =
+    Val (NonNegativeNonTopPolynomial.of_int_exn ?autoreleasepool_trace i)
+
 
   let make_trace_set ~map_above =
     AbstractDomain.StackedUtils.map
@@ -694,11 +789,6 @@ module NonNegativePolynomial = struct
       ~f_below:Fn.id
 
 
-  let get_symbols =
-    AbstractDomain.StackedUtils.map ~f:NonNegativeNonTopPolynomial.get_symbols ~f_above:Fn.id
-      ~f_below:Fn.id
-
-
   let pp_degree ~only_bigO fmt = function
     | Above _ ->
         Format.pp_print_string fmt "Top"
@@ -720,12 +810,12 @@ module NonNegativePolynomial = struct
         ""
 
 
-  let polynomial_traces p =
-    match get_symbols p with
+  let polynomial_traces ?is_autoreleasepool_trace = function
     | Below trace ->
         UnreachableTraces.make_err_trace trace
-    | Val symbols ->
-        List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces
+    | Val p ->
+        NonNegativeNonTopPolynomial.polynomial_traces ?is_autoreleasepool_trace p
+        |> Errlog.concat_traces
     | Above trace ->
         TopTraces.make_err_trace trace
 
diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli
index 89372612c..7f5176c87 100644
--- a/infer/src/bufferoverrun/polynomials.mli
+++ b/infer/src/bufferoverrun/polynomials.mli
@@ -22,7 +22,7 @@ end
 module NonNegativeNonTopPolynomial : sig
   type t
 
-  val get_symbols : t -> Bounds.NonNegativeBound.t list
+  val polynomial_traces : ?is_autoreleasepool_trace:bool -> t -> (string * Errlog.loc_trace) list
 end
 
 module TopTraces : sig
@@ -56,9 +56,9 @@ module NonNegativePolynomial : sig
 
   val zero : t
 
-  val one : t
+  val one : ?autoreleasepool_trace:Bounds.BoundTrace.t -> unit -> t
 
-  val of_int_exn : int -> t
+  val of_int_exn : ?autoreleasepool_trace:Bounds.BoundTrace.t -> int -> t
 
   val is_symbolic : t -> bool
 
@@ -91,7 +91,7 @@ module NonNegativePolynomial : sig
 
   val pp_degree : only_bigO:bool -> Format.formatter -> degree_with_term -> unit
 
-  val polynomial_traces : t -> Errlog.loc_trace
+  val polynomial_traces : ?is_autoreleasepool_trace:bool -> t -> Errlog.loc_trace
 
   val encode : t -> string
 
diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml
index e59e5f720..0ebe57413 100644
--- a/infer/src/cost/boundMap.ml
+++ b/infer/src/cost/boundMap.ml
@@ -36,7 +36,7 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
     let node_id = NodeCFG.Node.id node in
     match Procdesc.Node.get_kind node with
     | Procdesc.Node.Exit_node ->
-        Node.IdMap.add node_id BasicCost.one bound_map
+        Node.IdMap.add node_id (BasicCost.one ()) bound_map
     | _ -> (
         let exit_state_opt =
           let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in
@@ -63,7 +63,7 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
                      unreachable returning cost 0 \n" ;
                   BasicCost.of_unreachable node_loc
               | ExcRaised ->
-                  BasicCost.one
+                  BasicCost.one ()
               | Reachable mem ->
                   let cost =
                     BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) ~node_id
@@ -74,7 +74,7 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
                      values) does not make sense especially when the
                      abstract memory is non-bottom. This is a source
                      of unsoundness in the analysis. *)
-                  if BasicCost.is_zero cost then BasicCost.one else cost
+                  if BasicCost.is_zero cost then BasicCost.one () else cost
             in
             L.(debug Analysis Medium)
               "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id BasicCost.pp bound ;
diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml
index 466f390b1..21fa88a0b 100644
--- a/infer/src/cost/cost.ml
+++ b/infer/src/cost/cost.ml
@@ -57,8 +57,8 @@ module InstrBasicCostWithReason = struct
 
   let get_instr_cost_record tenv extras instr_node instr =
     match instr with
-    | Sil.Call (ret, Exp.Const (Const.Cfun callee_pname), params, _, _) when Config.inclusive_cost
-      ->
+    | Sil.Call (ret, Exp.Const (Const.Cfun callee_pname), params, location, _)
+      when Config.inclusive_cost ->
         let { inferbo_invariant_map
             ; integer_type_widths
             ; inferbo_get_summary
@@ -110,7 +110,10 @@ module InstrBasicCostWithReason = struct
         if is_allocation_function callee_pname then
           CostDomain.plus CostDomain.unit_cost_allocation operation_cost
         else if is_autorelease_function callee_pname then
-          CostDomain.plus CostDomain.unit_cost_autoreleasepool_size operation_cost
+          CostDomain.plus
+            (CostDomain.unit_cost_autoreleasepool_size
+               ~autoreleasepool_trace:(Bounds.BoundTrace.of_modeled_function "autorelease" location))
+            operation_cost
         else operation_cost
     | Sil.Call (_, Exp.Const (Const.Cfun _), _, _, _) ->
         CostDomain.zero_record
@@ -207,12 +210,19 @@ let is_report_suppressed pname =
 
 
 module Check = struct
-  let report_top_and_unreachable pname proc_desc err_log loc ~name ~cost
+  let report_top_and_unreachable kind pname proc_desc err_log loc ~name ~cost
       {CostIssues.unreachable_issue; infinite_issue} =
     let report issue suffix =
+      let is_autoreleasepool_trace =
+        match (kind : CostKind.t) with
+        | AutoreleasepoolSize ->
+            true
+        | OperationCost | AllocationCost ->
+            false
+      in
       let message = F.asprintf "%s of the function %a %s" name Procname.pp pname suffix in
       Reporting.log_issue proc_desc err_log ~loc
-        ~ltr:(BasicCostWithReason.polynomial_traces cost)
+        ~ltr:(BasicCostWithReason.polynomial_traces ~is_autoreleasepool_trace cost)
         ~extras:(compute_errlog_extras cost) Cost issue message
     in
     if BasicCostWithReason.is_top cost then report infinite_issue "cannot be computed"
@@ -226,9 +236,9 @@ module Check = struct
     let proc_loc = Procdesc.get_loc proc_desc in
     if not (is_report_suppressed pname) then
       CostIssues.CostKindMap.iter2 CostIssues.enabled_cost_map cost
-        ~f:(fun _kind (CostIssues.{name; top_and_unreachable} as issue_spec) cost ->
+        ~f:(fun kind (CostIssues.{name; top_and_unreachable} as issue_spec) cost ->
           if top_and_unreachable then
-            report_top_and_unreachable pname proc_desc err_log proc_loc ~name ~cost issue_spec )
+            report_top_and_unreachable kind pname proc_desc err_log proc_loc ~name ~cost issue_spec )
 end
 
 type bound_map = BasicCost.t Node.IdMap.t
diff --git a/infer/src/cost/costDomain.ml b/infer/src/cost/costDomain.ml
index cc39fec3f..c2bad9bed 100644
--- a/infer/src/cost/costDomain.ml
+++ b/infer/src/cost/costDomain.ml
@@ -13,7 +13,7 @@ module BasicCost = struct
 
   (* NOTE: Increment the version number if you changed the [t] type.  This is for avoiding
      demarshalling failure of cost analysis results in running infer-reportdiff. *)
-  let version = 7
+  let version = 8
 end
 
 module BasicCostWithReason = struct
@@ -25,7 +25,9 @@ module BasicCostWithReason = struct
 
   let zero = {cost= BasicCost.zero; top_pname_opt= None}
 
-  let one = {cost= BasicCost.one; top_pname_opt= None}
+  let one ?autoreleasepool_trace () =
+    {cost= BasicCost.one ?autoreleasepool_trace (); top_pname_opt= None}
+
 
   let subst callee_pname location record eval_sym =
     {record with cost= BasicCost.subst callee_pname location record.cost eval_sym}
@@ -42,7 +44,9 @@ module BasicCostWithReason = struct
 
   let mult_unreachable cost record = {record with cost= BasicCost.mult_unreachable cost record.cost}
 
-  let polynomial_traces {cost} = BasicCost.polynomial_traces cost
+  let polynomial_traces ~is_autoreleasepool_trace {cost} =
+    BasicCost.polynomial_traces ~is_autoreleasepool_trace cost
+
 
   let pp format {cost} = BasicCost.pp format cost
 
@@ -68,7 +72,8 @@ module VariantCostMap = struct
       record
 
 
-  let increment kind record = increase_by kind BasicCostWithReason.one record
+  let increment ?autoreleasepool_trace kind record =
+    increase_by kind (BasicCostWithReason.one ?autoreleasepool_trace ()) record
 end
 
 type t = VariantCostMap.t
@@ -119,8 +124,8 @@ let unit_cost_atomic_operation = VariantCostMap.increment CostKind.OperationCost
 
 let unit_cost_allocation = VariantCostMap.increment CostKind.AllocationCost zero_record
 
-let unit_cost_autoreleasepool_size =
-  VariantCostMap.increment CostKind.AutoreleasepoolSize zero_record
+let unit_cost_autoreleasepool_size ~autoreleasepool_trace =
+  VariantCostMap.increment ~autoreleasepool_trace CostKind.AutoreleasepoolSize zero_record
 
 
 let of_operation_cost operation_cost =
diff --git a/infer/src/cost/costDomain.mli b/infer/src/cost/costDomain.mli
index fe959f185..6edc9123d 100644
--- a/infer/src/cost/costDomain.mli
+++ b/infer/src/cost/costDomain.mli
@@ -39,7 +39,7 @@ module BasicCostWithReason : sig
 
   val degree : t -> Polynomials.Degree.t option
 
-  val polynomial_traces : t -> Errlog.loc_trace
+  val polynomial_traces : is_autoreleasepool_trace:bool -> t -> Errlog.loc_trace
 
   val pp_hum : Format.formatter -> t -> unit
 end
@@ -81,7 +81,7 @@ val unit_cost_atomic_operation : t
 val unit_cost_allocation : t
 (** Map representing cost record \{OperationCost:0; AllocationCost:1; AutoreleasepoolSize:0\} *)
 
-val unit_cost_autoreleasepool_size : t
+val unit_cost_autoreleasepool_size : autoreleasepool_trace:Bounds.BoundTrace.t -> t
 (** Map representing cost record \{OperationCost:0; AllocationCost:0; AutoreleasepoolSize:1\} *)
 
 val of_operation_cost : BasicCost.t -> t
diff --git a/infer/src/cost/costModels.ml b/infer/src/cost/costModels.ml
index 987be3bdd..9ba0d5467 100644
--- a/infer/src/cost/costModels.ml
+++ b/infer/src/cost/costModels.ml
@@ -9,7 +9,7 @@ open! IStd
 module BasicCost = CostDomain.BasicCost
 open BufferOverrunUtils.ModelEnv
 
-let unit_cost_model _model_env ~ret:_ _inferbo_mem = BasicCost.one
+let unit_cost_model _model_env ~ret:_ _inferbo_mem = BasicCost.one ()
 
 let cost_of_exp exp ~degree_kind ~of_function {integer_type_widths; location} ~ret:_ inferbo_mem =
   let itv =
diff --git a/infer/src/integration/Differential.ml b/infer/src/integration/Differential.ml
index 37295ae4b..c0ff73780 100644
--- a/infer/src/integration/Differential.ml
+++ b/infer/src/integration/Differential.ml
@@ -209,12 +209,13 @@ module CostItem = struct
       (pp_degree ~only_bigO:false) curr_item
 end
 
-let polynomial_traces = function
+let polynomial_traces issue_type = function
   | None ->
       []
   | Some (Val (_, degree_term)) ->
-      Polynomials.NonNegativeNonTopPolynomial.get_symbols degree_term
-      |> List.map ~f:Bounds.NonNegativeBound.make_err_trace
+      Polynomials.NonNegativeNonTopPolynomial.polynomial_traces
+        ~is_autoreleasepool_trace:(IssueType.is_autoreleasepool_size_issue issue_type)
+        degree_term
   | Some (Below traces) ->
       [("", Polynomials.UnreachableTraces.make_err_trace traces)]
   | Some (Above traces) ->
@@ -285,8 +286,10 @@ let issue_of_cost kind CostIssues.{complexity_increase_issue; unreachable_issue;
             (Format.asprintf "%s %a" msg CostItem.pp_cost_msg cost_item)
             [] ]
       in
-      (("", marker_cost_trace "Previous" prev_item) :: polynomial_traces prev_degree_with_term)
-      @ (("", marker_cost_trace "Updated" curr_item) :: polynomial_traces curr_degree_with_term)
+      ("", marker_cost_trace "Previous" prev_item)
+      :: polynomial_traces issue_type prev_degree_with_term
+      @ ("", marker_cost_trace "Updated" curr_item)
+        :: polynomial_traces issue_type curr_degree_with_term
       |> Errlog.concat_traces
     in
     let severity = IssueType.Advice in
diff --git a/infer/src/integration/JsonReports.ml b/infer/src/integration/JsonReports.ml
index dc36b70a9..6db151616 100644
--- a/infer/src/integration/JsonReports.ml
+++ b/infer/src/integration/JsonReports.ml
@@ -249,14 +249,16 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
               Format.asprintf "%a" (CostDomain.BasicCost.pp_degree ~only_bigO:true) degree_with_term
           }
         in
-        let cost_info cost =
+        let cost_info ?is_autoreleasepool_trace cost =
           { Jsonbug_t.polynomial_version= CostDomain.BasicCost.version
           ; polynomial= CostDomain.BasicCost.encode cost
           ; degree=
               Option.map (CostDomain.BasicCost.degree cost) ~f:Polynomials.Degree.encode_to_int
           ; hum= hum cost
-          ; trace= loc_trace_to_jsonbug_record (CostDomain.BasicCost.polynomial_traces cost) Advice
-          }
+          ; trace=
+              loc_trace_to_jsonbug_record
+                (CostDomain.BasicCost.polynomial_traces ?is_autoreleasepool_trace cost)
+                Advice }
         in
         let cost_item =
           let file =
@@ -269,7 +271,8 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
           ; is_on_ui_thread
           ; exec_cost= cost_info (CostDomain.get_cost_kind CostKind.OperationCost post).cost
           ; autoreleasepool_size=
-              cost_info (CostDomain.get_cost_kind CostKind.AutoreleasepoolSize post).cost }
+              cost_info ~is_autoreleasepool_trace:true
+                (CostDomain.get_cost_kind CostKind.AutoreleasepoolSize post).cost }
         in
         Some (Jsonbug_j.string_of_cost_item cost_item)
     | _ ->
diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml
index 87bea2ded..467632d46 100644
--- a/infer/src/istd/PrettyPrintable.ml
+++ b/infer/src/istd/PrettyPrintable.ml
@@ -253,6 +253,8 @@ module type PPUniqRankSet = sig
 
   val remove : elt -> t -> t
 
+  val mem : elt -> t -> bool
+
   val union_prefer_left : t -> t -> t
 
   val pp : ?print_rank:bool -> F.formatter -> t -> unit
@@ -319,6 +321,8 @@ module MakePPUniqRankSet
 
   let remove value map = Map.remove (Val.to_rank value) map
 
+  let mem value map = Map.mem (Val.to_rank value) map
+
   let singleton value = add Map.empty value
 
   let union_prefer_left m1 m2 = Map.union (fun _rank value1 _value2 -> Some value1) m1 m2
diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli
index 259397b6c..83c526154 100644
--- a/infer/src/istd/PrettyPrintable.mli
+++ b/infer/src/istd/PrettyPrintable.mli
@@ -204,6 +204,8 @@ module type PPUniqRankSet = sig
 
   val remove : elt -> t -> t
 
+  val mem : elt -> t -> bool
+
   val union_prefer_left : t -> t -> t
   (** in case an element with the same rank is present both in [lhs] and [rhs], keep the one from
       [lhs] in [union_prefer_left lhs rhs] *)
diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
index d4ab84070..05f3d5dba 100644
--- a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
+++ b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
@@ -1,17 +1,17 @@
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callAllocObject_zero:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callCopyObject_zero:x:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callGiveMeObject_autoreleasepool_zero:, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callGiveMeObject_linear:, n,  OnUIThread:false, [{n},Loop]
+codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callGiveMeObject_linear:, n,  OnUIThread:false, [{n},Loop,autorelease,Call to NoArcCallee.giveMeObject,Modeled call to autorelease]
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callMutableCopyObject_zero:x:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callNewObject_zero:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.dealloc, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.autorelease_unreachable_zero:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_autoreleasepool_zero:, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_linear:, n,  OnUIThread:false, [{n},Loop]
+codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_linear:, n,  OnUIThread:false, [{n},Loop,autorelease,Call to Basic.call_autorelease_constant,Modeled call to autorelease]
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_nested_zero:, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_sequential_constant:, 1,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_sequential_linear:, n,  OnUIThread:false, [{n},Loop]
-codetoanalyze/objc/autoreleasepool/basic.m, Basic.call_autorelease_constant, 1,  OnUIThread:false, []
+codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_sequential_constant:, 1,  OnUIThread:false, [autorelease,Call to Basic.call_autorelease_constant,Modeled call to autorelease]
+codetoanalyze/objc/autoreleasepool/basic.m, Basic.autoreleased_in_loop_sequential_linear:, n,  OnUIThread:false, [{n},Loop,autorelease,Call to Basic.call_autorelease_constant,Modeled call to autorelease]
+codetoanalyze/objc/autoreleasepool/basic.m, Basic.call_autorelease_constant, 1,  OnUIThread:false, [autorelease,Modeled call to autorelease]
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.call_no_autorelease_zero, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.dealloc, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/basic.m, Basic.loop_in_autoreleasepool_zero:, 0,  OnUIThread:false, []
@@ -19,6 +19,6 @@ codetoanalyze/objc/autoreleasepool/basic.m, Basic.no_autoreleased_in_loop_zero:,
 codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.allocObject, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.copyObject:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.dealloc, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.giveMeObject, 1,  OnUIThread:false, []
+codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.giveMeObject, 1,  OnUIThread:false, [autorelease,Modeled call to autorelease]
 codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.mutableCopyObject:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/no_arc_callee.m, NoArcCallee.newObject, 0,  OnUIThread:false, []