diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index fed33b2b4..512595e26 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -319,13 +319,15 @@ module Heap = struct
     if is_empty mem then Val.bot else snd (choose mem)
 
 
-  let range : filter_loc:(Loc.t -> bool) -> astate -> Itv.NonNegativeBound.t =
+  let range : filter_loc:(Loc.t -> bool) -> astate -> Itv.NonNegativePolynomial.astate =
    fun ~filter_loc mem ->
     fold
       (fun loc v acc ->
-        if filter_loc loc then v |> Val.get_itv |> Itv.range |> Itv.NonNegativeBound.mult acc
+        if filter_loc loc then
+          v |> Val.get_itv |> Itv.range |> Itv.ItvRange.to_top_lifted_polynomial
+          |> Itv.NonNegativePolynomial.mult acc
         else acc )
-      mem Itv.NonNegativeBound.one
+      mem Itv.NonNegativePolynomial.one
 end
 
 module AliasTarget = struct
@@ -766,7 +768,7 @@ module MemReach = struct
     fun locs m -> add_from_locs m.heap locs PowLoc.empty
 
 
-  let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativeBound.t =
+  let heap_range : filter_loc:(Loc.t -> bool) -> t -> Itv.NonNegativePolynomial.astate =
    fun ~filter_loc {heap} -> Heap.range ~filter_loc heap
 end
 
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 84329247a..445e6181e 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -150,6 +150,89 @@ end = struct
     num / den
 end
 
+module Ints : sig
+  module NonNegativeInt : sig
+    type t = private int [@@deriving compare]
+
+    val zero : t
+
+    val one : t
+
+    val of_int_exn : int -> t
+
+    val is_zero : t -> bool
+
+    val is_one : t -> bool
+
+    val ( <= ) : lhs:t -> rhs:t -> bool
+
+    val ( + ) : t -> t -> t
+
+    val ( * ) : t -> t -> t
+
+    val max : t -> t -> t
+
+    val min : t -> t -> t
+
+    val pp : F.formatter -> t -> unit
+  end
+
+  module PositiveInt : sig
+    type t = private NonNegativeInt.t [@@deriving compare]
+
+    val one : t
+
+    val of_int : int -> t option
+
+    val succ : t -> t
+
+    val pp : F.formatter -> t -> unit
+  end
+end = struct
+  module NonNegativeInt = struct
+    type t = int [@@deriving compare]
+
+    let zero = 0
+
+    let one = 1
+
+    let is_zero = function 0 -> true | _ -> false
+
+    let is_one = function 1 -> true | _ -> false
+
+    let of_int_exn i =
+      assert (i >= 0) ;
+      i
+
+
+    let ( <= ) ~lhs ~rhs = Int.(lhs <= rhs)
+
+    let ( + ) = Int.( + )
+
+    let ( * ) = Int.( * )
+
+    let max = Int.max
+
+    let min = Int.min
+
+    let pp = F.pp_print_int
+  end
+
+  module PositiveInt = struct
+    type t = NonNegativeInt.t [@@deriving compare]
+
+    let one = 1
+
+    let of_int i = if i <= 0 then None else Some i
+
+    let succ = Int.succ
+
+    let pp = F.pp_print_int
+  end
+end
+
+open Ints
+
 module SymLinear = struct
   module M = SymbolMap
 
@@ -723,8 +806,6 @@ module Bound = struct
         if le y x then x else PInf
 
 
-  let ( <= ) ~lhs ~rhs = le lhs rhs
-
   let zero : t = Linear (0, SymLinear.zero)
 
   let one : t = Linear (1, SymLinear.zero)
@@ -873,83 +954,313 @@ module Bound = struct
   let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
 end
 
+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 astate = t
-
   let pp = Bound.pp
 
   let zero = Bound.zero
 
-  let one = Bound.one
-
-  let top = Bound.PInf
-
   let of_bound b = if Bound.le b Bound.zero then Bound.zero else b
 
-  let of_int_exn i =
-    assert (i >= 0) ;
-    Bound.of_int i
-
-
-  let is_not_infty = function
+  let classify = function
     | Bound.PInf ->
-        false
-    | Bound.(Linear _ | MinMax _) ->
-        true
+        ValTop
     | Bound.MInf ->
         assert false
+    | b ->
+      match Bound.is_const b with
+      | None ->
+          Symbolic b
+      | Some c ->
+          Constant (NonNegativeInt.of_int_exn c)
 
 
-  let is_symbolic = Bound.is_symbolic
+  let subst b map =
+    match Bound.subst_ub b map with
+    | Bottom ->
+        Constant NonNegativeInt.zero
+    | NonBottom b ->
+        of_bound b |> classify
+end
 
-  let ( <= ) = Bound.( <= )
+module type NonNegativeSymbol = sig
+  type t [@@deriving compare]
 
-  (* For now let's check and fail when these operations don't give a non-negative result *)
+  val subst : t -> Bound.t bottom_lifted SymbolMap.t -> (NonNegativeInt.t, t) valclass
+
+  val pp : F.formatter -> t -> unit
+end
+
+module MakePolynomial (S : NonNegativeSymbol) = struct
+  module M = struct
+    include Caml.Map.Make (S)
+
+    let increasing_union ~f m1 m2 = union (fun _ v1 v2 -> Some (f v1 v2)) m1 m2
+
+    let inter ~f m1 m2 =
+      merge
+        (fun _ v1_opt v2_opt ->
+          match (v1_opt, v2_opt) with Some v1, Some v2 -> f v1 v2 | _ -> None )
+        m1 m2
+
+
+    let le ~le_elt m1 m2 =
+      match
+        merge
+          (fun _ v1_opt v2_opt ->
+            match (v1_opt, v2_opt) with
+            | Some _, None ->
+                raise Exit
+            | Some lhs, Some rhs when not (le_elt ~lhs ~rhs) ->
+                raise Exit
+            | _ ->
+                None )
+          m1 m2
+      with
+      | _ ->
+          true
+      | exception Exit ->
+          false
+  end
+
+  (** If x < y < z then
+    2 + 3 * x + 4 * x ^ 2 + x * y + 7 * y ^ 2 * z
+    is represented by
+    {const= 2; terms= {
+      x -> {const= 3; terms= {
+        x -> {const= 4; terms={}},
+        y -> {const= 1; terms={}}
+      }},
+      y -> {const= 0; terms= {
+        y -> {const= 0; terms= {
+          z -> {const= 7; terms={}}
+        }}
+      }}
+    }}
+
+    The representation is a tree, each edge from a node to a child (terms) represents a multiplication by a symbol. If a node has a non-zero const, it represents the multiplication (of the path) by this constant.
+    In the example above, we have the following paths:
+    2
+    x * 3
+    x * x * 4
+    x * y * 1
+    y * y * z * 7
+
+    Invariants:
+      - except for the root, terms <> {} \/ const <> 0
+      - 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}
+
+  type astate = t
 
-  let checked1 name f b =
-    let res = f b in
-    let () =
-      if Bound.lt res zero then
-        L.internal_error "NonNegativeBound.%s %a = %a < 0@\n" name pp b pp res
+  let of_non_negative_int : NonNegativeInt.t -> t = fun const -> {const; terms= M.empty}
+
+  let zero = of_non_negative_int NonNegativeInt.zero
+
+  let one = of_non_negative_int NonNegativeInt.one
+
+  let of_int_exn : int -> t = fun i -> i |> NonNegativeInt.of_int_exn |> of_non_negative_int
+
+  let of_valclass : (NonNegativeInt.t, S.t) valclass -> t top_lifted = function
+    | ValTop ->
+        Top
+    | Constant i ->
+        NonTop (of_non_negative_int i)
+    | Symbolic s ->
+        NonTop {const= NonNegativeInt.zero; terms= M.singleton s one}
+
+
+  let is_zero : t -> bool = fun {const; terms} -> NonNegativeInt.is_zero const && M.is_empty terms
+
+  let is_one : t -> bool = fun {const; terms} -> NonNegativeInt.is_one const && M.is_empty terms
+
+  let non_zero : t -> t option = fun p -> if is_zero p then None else Some p
+
+  let is_symbolic : t -> bool = fun {terms} -> not (M.is_empty terms)
+
+  let rec plus : t -> t -> t =
+   fun p1 p2 ->
+    { const= NonNegativeInt.(p1.const + p2.const)
+    ; terms= M.increasing_union ~f:plus p1.terms p2.terms }
+
+
+  let rec mult_const_positive : t -> PositiveInt.t -> t =
+   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 =
+   fun p c ->
+    match PositiveInt.of_int (c :> int) with None -> zero | 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 =
+   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 s_term =
+      let terms =
+        match equal_s_opt with
+        | None ->
+            greater_than_s
+        | Some equal_s_p ->
+            M.add s equal_s_p greater_than_s
+      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
+    {const= NonNegativeInt.zero; terms}
+
+
+  let rec mult : t -> t -> t =
+   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
+    else
+      mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms
+
+
+  (* assumes symbols are not comparable *)
+  let rec ( <= ) : lhs:t -> rhs:t -> bool =
+   fun ~lhs ~rhs ->
+    NonNegativeInt.( <= ) ~lhs:lhs.const ~rhs:rhs.const && M.le ~le_elt:( <= ) lhs.terms rhs.terms
+
+
+  (* Possible optimization for later: x join x^2 = x^2 instead of x + x^2 *)
+  let rec join : t -> t -> t =
+   fun p1 p2 ->
+    { const= NonNegativeInt.max p1.const p2.const
+    ; terms= M.increasing_union ~f:join p1.terms p2.terms }
+
+
+  let rec min : t -> t -> t =
+   fun p1 p2 ->
+    {const= NonNegativeInt.min p1.const p2.const; terms= M.inter ~f:min_non_zero p1.terms p2.terms}
+
+
+  and min_non_zero : t -> t -> t option = fun p1 p2 -> min p1 p2 |> non_zero
+
+  let widen : prev:t -> next:t -> num_iters:int -> t =
+   fun ~prev:_ ~next:_ ~num_iters:_ -> assert false
+
+
+  let subst =
+    let exception ReturnTop in
+    (* avoids top-lifting everything *)
+    let rec subst {const; terms} map =
+      M.fold
+        (fun s p acc ->
+          match S.subst s map with
+          | Constant c -> (
+            match PositiveInt.of_int (c :> int) with
+            | None ->
+                acc
+            | Some c ->
+                let p = subst p map in
+                mult_const_positive p c |> plus acc )
+          | ValTop ->
+              let p = subst p map in
+              if is_zero p then acc else raise ReturnTop
+          | Symbolic s ->
+              let p = subst p map in
+              mult_symb p s |> plus acc )
+        terms (of_non_negative_int const)
     in
-    res
+    fun p map -> match subst p map with p -> NonTop p | exception ReturnTop -> Top
 
 
-  let checked2 name f b1 b2 =
-    let res = f b1 b2 in
-    let () =
-      if Bound.lt res zero then
-        L.internal_error "NonNegativeBound.%s %a %a = %a < 0@\n" name pp b1 pp b2 pp res
+  let pp : F.formatter -> t -> 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)
+    in
+    let pp_coeff fmt (c: NonNegativeInt.t) =
+      if (c :> int) > 1 then F.fprintf fmt "%a * " NonNegativeInt.pp c
+    in
+    let pp_exp fmt (e: PositiveInt.t) =
+      if (e :> int) > 1 then F.fprintf fmt "^%a" PositiveInt.pp e
+    in
+    let pp_magic_parentheses pp fmt x =
+      let s = F.asprintf "%a" pp x in
+      if String.contains s ' ' then F.fprintf fmt "(%s)" s else F.pp_print_string fmt s
     in
-    res
+    let pp_symb fmt symb = pp_magic_parentheses S.pp fmt symb in
+    let pp_symb_exp fmt (symb, exp) = F.fprintf fmt "%a%a" pp_symb symb pp_exp exp in
+    let pp_symbs fmt (last, others) =
+      List.rev_append others [last] |> Pp.seq ~sep:" * " pp_symb_exp fmt
+    in
+    let rec pp_sub symbs fmt {const; terms} =
+      if not (NonNegativeInt.is_zero const) then
+        F.fprintf fmt " + %a%a" pp_coeff const pp_symbs symbs ;
+      M.iter (fun s p -> pp_sub (add_symb s symbs) fmt p) terms
+    in
+    fun fmt {const; terms} ->
+      NonNegativeInt.pp fmt const ;
+      M.iter (fun s p -> pp_sub ((s, PositiveInt.one), []) fmt p) terms
+end
 
+module NonNegativePolynomial = struct
+  module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBound)
+  include AbstractDomain.TopLifted (NonNegativeNonTopPolynomial)
 
-  let join b1 b2 = checked2 "join" Bound.max_u b1 b2
+  let zero = NonTop NonNegativeNonTopPolynomial.zero
 
-  let min b1 b2 = checked2 "min" Bound.min_u b1 b2
+  let one = NonTop NonNegativeNonTopPolynomial.one
 
-  let mult : t -> t -> t =
-   fun x y ->
-    match (x, Bound.is_const x, y, Bound.is_const y) with
-    | x, _, _, Some n | _, Some n, x, _ -> (
-      match NonZeroInt.of_int n with
-      | Some n ->
-          if NonZeroInt.is_one n then x
-          else if NonZeroInt.is_minus_one n then assert false
-          else checked1 "neg(mult_const)" (Bound.mult_const_u n) x
-      | None ->
-          zero )
-    | _ ->
-        top
+  let of_int_exn i = NonTop (NonNegativeNonTopPolynomial.of_int_exn i)
+
+  let of_non_negative_bound b =
+    b |> NonNegativeBound.classify |> NonNegativeNonTopPolynomial.of_valclass
+
+
+  let is_symbolic = function Top -> false | NonTop p -> NonNegativeNonTopPolynomial.is_symbolic p
 
+  let is_top = function Top -> true | _ -> false
 
-  let plus b1 b2 = checked2 "plus" Bound.plus_u b1 b2
+  let top_lifted_increasing ~f p1 p2 =
+    match (p1, p2) with Top, _ | _, Top -> Top | NonTop p1, NonTop p2 -> NonTop (f p1 p2)
 
-  let widen ~prev ~next ~num_iters:_ = checked2 "widen" Bound.widen_u prev next
 
-  let subst b map = match Bound.subst_ub b map with Bottom -> zero | NonBottom b -> of_bound b
+  let plus = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.plus
+
+  let mult = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.mult
+
+  let min p1 p2 =
+    match (p1, p2) with
+    | Top, x | x, Top ->
+        x
+    | NonTop p1, NonTop p2 ->
+        NonTop (NonNegativeNonTopPolynomial.min p1 p2)
+
+
+  let widen ~prev ~next ~num_iters:_ = if ( <= ) ~lhs:next ~rhs:prev then prev else Top
+
+  let subst p map = match p with Top -> Top | NonTop p -> NonNegativeNonTopPolynomial.subst p map
+end
+
+module ItvRange = struct
+  type t = NonNegativeBound.t
+
+  let zero : t = NonNegativeBound.zero
+
+  let of_bounds : lb:Bound.t -> ub:Bound.t -> t =
+   fun ~lb ~ub ->
+    Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb) |> NonNegativeBound.of_bound
+
+
+  let to_top_lifted_polynomial : t -> NonNegativePolynomial.astate =
+   fun r -> NonNegativePolynomial.of_non_negative_bound r
 end
 
 module ItvPure = struct
@@ -1082,9 +1393,7 @@ module ItvPure = struct
 
   let is_le_zero : t -> bool = fun (_, ub) -> Bound.le ub Bound.zero
 
-  let range : t -> NonNegativeBound.t =
-   fun (l, u) -> Bound.plus_u (Bound.plus_u u Bound.one) (Bound.neg l) |> NonNegativeBound.of_bound
-
+  let range : t -> ItvRange.t = fun (lb, ub) -> ItvRange.of_bounds ~lb ~ub
 
   let neg : t -> t =
    fun (l, u) ->
@@ -1427,7 +1736,12 @@ 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 -> Bound.t = function Bottom -> Bound.zero | NonBottom itv -> ItvPure.range itv
+let range : t -> ItvRange.t = function
+  | Bottom ->
+      ItvRange.zero
+  | NonBottom itv ->
+      ItvPure.range itv
+
 
 let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t =
  fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x)
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index d3c2167f9..40fe33be0 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/infer/src/bufferoverrun/itv.mli
@@ -57,39 +57,32 @@ module Bound : sig
   val lt : t -> t -> bool
 end
 
-(** 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 : sig
-  type t
-
-  type astate = t
-
-  val pp : F.formatter -> t -> unit
-
-  val zero : t
-
-  val one : t
+module NonNegativePolynomial : sig
+  include AbstractDomain.WithTop
 
-  val top : t
+  val zero : astate
 
-  val of_int_exn : int -> t
+  val one : astate
 
-  val is_not_infty : t -> bool
+  val of_int_exn : int -> astate
 
-  val is_symbolic : t -> bool
+  val is_symbolic : astate -> bool
 
-  val ( <= ) : lhs:t -> rhs:t -> bool
+  val is_top : astate -> bool
 
-  val join : t -> t -> t
+  val plus : astate -> astate -> astate
 
-  val min : t -> t -> t
+  val mult : astate -> astate -> astate
 
-  val mult : t -> t -> t
+  val min : astate -> astate -> astate
 
-  val plus : t -> t -> t
+  val subst : astate -> Bound.t bottom_lifted SymbolMap.t -> astate
+end
 
-  val widen : prev:t -> next:t -> num_iters:'a -> t
+module ItvRange : sig
+  type t
 
-  val subst : t -> Bound.t bottom_lifted SymbolMap.t -> t
+  val to_top_lifted_polynomial : t -> NonNegativePolynomial.astate
 end
 
 module ItvPure : sig
@@ -204,7 +197,7 @@ val le : lhs:t -> rhs:t -> bool
 
 val lnot : t -> Boolean.t
 
-val range : t -> NonNegativeBound.t
+val range : t -> ItvRange.t
 
 val div : t -> t -> t
 
diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml
index 6ec55c45e..1747f3d84 100644
--- a/infer/src/checkers/cost.ml
+++ b/infer/src/checkers/cost.ml
@@ -470,7 +470,7 @@ module TransferFunctionsWCET = struct
   (* We don't report when the cost is Top as it corresponds to subsequent 'don't know's.
    Instead, we report Top cost only at the top level per function when `report_infinity` is set to true *)
   let should_report_cost cost =
-    BasicCost.is_not_infty cost && not (BasicCost.( <= ) ~lhs:cost ~rhs:expensive_threshold)
+    not (BasicCost.is_top cost) && not (BasicCost.( <= ) ~lhs:cost ~rhs:expensive_threshold)
 
 
   let do_report summary loc cost =
@@ -556,7 +556,7 @@ end
 module AnalyzerWCET = AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsWCET)
 
 let check_and_report_infinity cost proc_desc summary =
-  if not (BasicCost.is_not_infty cost) then
+  if BasicCost.is_top cost then
     let loc = Procdesc.get_start_node proc_desc |> Procdesc.Node.get_loc in
     let message =
       F.asprintf "The execution time of the function %a cannot be computed" Typ.Procname.pp
diff --git a/infer/src/checkers/costDomain.ml b/infer/src/checkers/costDomain.ml
index 44d4dbacb..f8f4936e8 100644
--- a/infer/src/checkers/costDomain.ml
+++ b/infer/src/checkers/costDomain.ml
@@ -9,7 +9,7 @@
 
 open! IStd
 module F = Format
-module BasicCost = Itv.NonNegativeBound
+module BasicCost = Itv.NonNegativePolynomial
 
 (** Map (node,instr) -> basic cost  *)
 module NodeInstructionToCostMap = AbstractDomain.MapOfPPMap (ProcCfg.InstrNode.IdMap) (BasicCost)
diff --git a/infer/tests/codetoanalyze/c/performance/instantiate.c b/infer/tests/codetoanalyze/c/performance/instantiate.c
index 8020fdc96..91521d294 100644
--- a/infer/tests/codetoanalyze/c/performance/instantiate.c
+++ b/infer/tests/codetoanalyze/c/performance/instantiate.c
@@ -18,3 +18,15 @@ void do_n_times(int n) {
 void do_2_times_Good() { do_n_times(2); }
 
 void do_2K_times_Bad() { do_n_times(2000); }
+
+void do_m2_times(int m) {
+  for (int i = 0; i < m; i++) {
+    do_n_times(m);
+  }
+}
+
+void do_half_m2_times(int m) {
+  for (int i = 0; i < m; i++) {
+    do_n_times(i);
+  }
+}
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index 06745414f..1b4bed5f8 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -4,13 +4,12 @@ codetoanalyze/c/performance/cost_test.c, loop0_bad, 5, EXPENSIVE_EXECUTION_TIME_
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1104]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1106]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 11xs$1 + 3]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -s$0 + s$1 + 16]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -13xs$0 + 13xs$1 + 199]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -13xs$0 + 13xs$1 + 199]
-codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost -15xs$0 + 15xs$1 + 231]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 11 * s$1]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 11 * s$1]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 11 * s$1]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 11 * (-s$0 + s$1 + 15)]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 4 + 11 * (-s$0 + s$1 + 15)]
+codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 11 * (-s$0 + s$1 + 15)]
 codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 211]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 12, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 201]
 codetoanalyze/c/performance/cost_test_deps.c, loop_despite_inferbo, 3, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 1204]
@@ -31,5 +30,9 @@ codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 8, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 545]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 547]
 codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 12004]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6xs$1 + 3]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6xs$1 + 3]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * (s$1 + -1) * s$1 + 10 * s$1]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * (s$1 + -1) * s$1 + 10 * s$1]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 10 * s$1 + 6 * s$1^2]
+codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 10 * s$1 + 6 * s$1^2]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * s$1]
+codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 3 + 6 * s$1]
diff --git a/infer/tests/codetoanalyze/java/performance/ArrayCost.java b/infer/tests/codetoanalyze/java/performance/ArrayCost.java
index 81f68ebc7..1465b527c 100644
--- a/infer/tests/codetoanalyze/java/performance/ArrayCost.java
+++ b/infer/tests/codetoanalyze/java/performance/ArrayCost.java
@@ -8,7 +8,7 @@
  */
 public class ArrayCost {
 
-  private void ArrayCost_FP(int[] mag) {
+  private void ArrayCost(int[] mag) {
 
     int i = 0;
     int k = mag.length;
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 1686e353e..ce68be224 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -1,5 +1,6 @@
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
-codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost_FP(int[]), 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
+codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 6 + 5 * s$7^2]
+codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, ERROR, [with estimated cost 5 + 5 * s$7^2]
 codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,Object), 0, INFINITE_EXECUTION_TIME_CALL, ERROR, []