diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 211f3b440..3176a413d 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -261,8 +261,8 @@ module Bound = struct
 
   let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
 
-  let of_path path_of_partial bound_end ~unsigned partial =
-    let s = Symb.Symbol.make ~unsigned (path_of_partial partial) bound_end in
+  let of_path path_of_partial make_symbol ~unsigned partial =
+    let s = make_symbol ~unsigned (path_of_partial partial) in
     of_sym (SymLinear.singleton_one s)
 
 
@@ -826,22 +826,25 @@ module Bound = struct
           NonBottom (f x y)
     in
     fun ~subst_pos x eval_sym ->
-      let get s =
-        match eval_sym s with
+      let get s bound_position =
+        match eval_sym s bound_position with
         | NonBottom x when Symb.Symbol.is_unsigned s ->
             NonBottom (approx_max subst_pos x zero)
         | x ->
             x
       in
       let get_mult_const s coeff =
-        if NonZeroInt.is_one coeff then get s
-        else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg
+        let bound_position =
+          if NonZeroInt.is_positive coeff then subst_pos else Symb.BoundEnd.neg subst_pos
+        in
+        if NonZeroInt.is_one coeff then get s bound_position
+        else if NonZeroInt.is_minus_one coeff then get s bound_position |> lift1 neg
         else
-          match eval_sym s with
+          match eval_sym s bound_position with
           | Bottom -> (
-            (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *)
-            match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
-            | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
+            (* For unsigned symbols, we can over/under-approximate with zero depending on [bound_position]. *)
+            match (Symb.Symbol.is_unsigned s, bound_position) with
+            | true, Symb.BoundEnd.LowerBound ->
                 NonBottom zero
             | _ ->
                 Bottom )
@@ -860,62 +863,65 @@ module Bound = struct
               ~init:(NonBottom (of_big_int c))
               ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
       | MinMax (c, sign, min_max, d, s) -> (
-        match get s with
-        | Bottom ->
-            Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
-                NonBottom (of_big_int i) )
-        | NonBottom x' ->
-            let res =
-              match (sign, min_max, x') with
-              | Plus, Min, MInf | Minus, Max, PInf ->
-                  MInf
-              | Plus, Max, PInf | Minus, Min, MInf ->
-                  PInf
-              | sign, Min, PInf | sign, Max, MInf ->
-                  of_big_int (Sign.eval_big_int sign c d)
-              | _, _, Linear (c2, se) -> (
-                  if SymLinear.is_zero se then
-                    of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
-                  else if SymLinear.is_one_symbol se then
-                    mk_MinMax
-                      ( Sign.eval_big_int sign c c2
-                      , sign
-                      , min_max
-                      , Z.(d - c2)
-                      , SymLinear.get_one_symbol se )
-                  else if SymLinear.is_mone_symbol se then
-                    mk_MinMax
-                      ( Sign.eval_big_int sign c c2
-                      , Sign.neg sign
-                      , MinMax.neg min_max
-                      , Z.(c2 - d)
-                      , SymLinear.get_mone_symbol se )
-                  else
-                    match big_int_of_minmax subst_pos x with
-                    | Some i ->
-                        of_big_int i
-                    | None ->
-                        of_bound_end subst_pos )
-              | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
-                match (min_max, sign2, min_max2) with
-                | Min, Plus, Min | Max, Plus, Max ->
-                    let c' = Sign.eval_big_int sign c c2 in
-                    let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
-                    mk_MinMax (c', sign, min_max, d', s2)
-                | Min, Minus, Max | Max, Minus, Min ->
-                    let c' = Sign.eval_big_int sign c c2 in
-                    let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
-                    mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
-                | _ ->
-                    let bound_end =
-                      match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
-                    in
-                    of_big_int
-                      (Sign.eval_big_int sign c
-                         (MinMax.eval_big_int min_max d
-                            (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
-            in
-            NonBottom res )
+          let bound_position =
+            match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
+          in
+          match get s bound_position with
+          | Bottom ->
+              Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
+                  NonBottom (of_big_int i) )
+          | NonBottom x' ->
+              let res =
+                match (sign, min_max, x') with
+                | Plus, Min, MInf | Minus, Max, PInf ->
+                    MInf
+                | Plus, Max, PInf | Minus, Min, MInf ->
+                    PInf
+                | sign, Min, PInf | sign, Max, MInf ->
+                    of_big_int (Sign.eval_big_int sign c d)
+                | _, _, Linear (c2, se) -> (
+                    if SymLinear.is_zero se then
+                      of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
+                    else if SymLinear.is_one_symbol se then
+                      mk_MinMax
+                        ( Sign.eval_big_int sign c c2
+                        , sign
+                        , min_max
+                        , Z.(d - c2)
+                        , SymLinear.get_one_symbol se )
+                    else if SymLinear.is_mone_symbol se then
+                      mk_MinMax
+                        ( Sign.eval_big_int sign c c2
+                        , Sign.neg sign
+                        , MinMax.neg min_max
+                        , Z.(c2 - d)
+                        , SymLinear.get_mone_symbol se )
+                    else
+                      match big_int_of_minmax subst_pos x with
+                      | Some i ->
+                          of_big_int i
+                      | None ->
+                          of_bound_end subst_pos )
+                | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
+                  match (min_max, sign2, min_max2) with
+                  | Min, Plus, Min | Max, Plus, Max ->
+                      let c' = Sign.eval_big_int sign c c2 in
+                      let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
+                      mk_MinMax (c', sign, min_max, d', s2)
+                  | Min, Minus, Max | Max, Minus, Min ->
+                      let c' = Sign.eval_big_int sign c c2 in
+                      let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
+                      mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
+                  | _ ->
+                      let bound_end =
+                        match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
+                      in
+                      of_big_int
+                        (Sign.eval_big_int sign c
+                           (MinMax.eval_big_int min_max d
+                              (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
+              in
+              NonBottom res )
 
 
   let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index 56608c1f4..9a7ccd427 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/infer/src/bufferoverrun/bounds.mli
@@ -43,11 +43,17 @@ module Bound : sig
 
   val _255 : t
 
-  val of_normal_path : Symb.BoundEnd.t -> unsigned:bool -> Symb.SymbolPath.partial -> t
+  val of_normal_path :
+       (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t)
+    -> unsigned:bool
+    -> Symb.SymbolPath.partial
+    -> t
 
-  val of_offset_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
+  val of_offset_path :
+    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
-  val of_length_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
+  val of_length_path :
+    (unsigned:bool -> Symb.SymbolPath.t -> Symb.Symbol.t) -> Symb.SymbolPath.partial -> t
 
   val is_symbolic : t -> bool
 
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index d6ef2be9e..3e0504033 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -392,10 +392,11 @@ let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =
     let actuals = List.map ~f:(fun (a, _) -> eval integer_type_widths a caller_mem) actual_exps in
     ParamBindings.make formals actuals
   in
-  let eval_sym s =
+  let eval_sym s bound_end =
     let sympath = Symb.Symbol.path s in
     let itv, _ = eval_sympath params sympath caller_mem in
-    Itv.get_bound itv (Symb.Symbol.bound_end s)
+    Symb.Symbol.assert_bound_end s bound_end ;
+    Itv.get_bound itv bound_end
   in
   let trace_of_sym s =
     let sympath = Symb.Symbol.path s in
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index e2647d19f..f18d27b53 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/infer/src/bufferoverrun/itv.ml
@@ -411,9 +411,13 @@ module ItvPure = struct
 
 
   let of_path bound_of_path path =
-    let lb = bound_of_path Symb.BoundEnd.LowerBound path in
-    let ub = bound_of_path Symb.BoundEnd.UpperBound path in
-    (lb, ub)
+    if Symb.SymbolPath.represents_multiple_values_sound path then
+      let lb = bound_of_path (Symb.Symbol.make_boundend Symb.BoundEnd.LowerBound) path in
+      let ub = bound_of_path (Symb.Symbol.make_boundend Symb.BoundEnd.UpperBound) path in
+      (lb, ub)
+    else
+      let b = bound_of_path Symb.Symbol.make_onevalue path in
+      (b, b)
 
 
   let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)
diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml
index bda3f55ed..a331d3753 100644
--- a/infer/src/bufferoverrun/symb.ml
+++ b/infer/src/bufferoverrun/symb.ml
@@ -10,6 +10,8 @@ module F = Format
 module BoundEnd = struct
   type t = LowerBound | UpperBound [@@deriving compare]
 
+  let equal = [%compare.equal: t]
+
   let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
 
   let to_string = function LowerBound -> "lb" | UpperBound -> "ub"
@@ -92,6 +94,8 @@ module SymbolPath = struct
         F.fprintf fmt "%a.length" pp_partial p
 
 
+  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
+
   let rec represents_multiple_values = function
     (* TODO depending on the result, the call might represent multiple values *)
     | Callsite _ | Pvar _ ->
@@ -105,6 +109,17 @@ module SymbolPath = struct
         represents_multiple_values p
 
 
+  let rec represents_multiple_values_sound = function
+    | Callsite _ ->
+        true
+    | Pvar _ ->
+        false
+    | Deref ((Deref_ArrayIndex | Deref_CPointer), _) ->
+        true
+    | Deref (Deref_JavaPointer, p) | Field (_, p) ->
+        represents_multiple_values_sound p
+
+
   let rec represents_callsite_sound_partial = function
     | Callsite _ ->
         true
@@ -112,9 +127,6 @@ module SymbolPath = struct
         false
     | Deref (_, p) | Field (_, p) ->
         represents_callsite_sound_partial p
-
-
-  let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 end
 
 module Symbol = struct
@@ -122,38 +134,67 @@ module Symbol = struct
 
   let compare_extra_bool _ _ = 0
 
-  type t = {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t} [@@deriving compare]
+  type t =
+    | OneValue of {unsigned: extra_bool; path: SymbolPath.t}
+    | BoundEnd of {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t}
+  [@@deriving compare]
 
-  let compare x y =
-    let r = compare x y in
-    if Int.equal r 0 then assert (Bool.equal x.unsigned y.unsigned) ;
-    r
+  let compare s1 s2 =
+    match (s1, s2) with
+    | OneValue _, BoundEnd _ ->
+        -1
+    | BoundEnd _, OneValue _ ->
+        1
+    | OneValue {unsigned= unsigned1}, OneValue {unsigned= unsigned2}
+    | BoundEnd {unsigned= unsigned1}, BoundEnd {unsigned= unsigned2} ->
+        let r = compare s1 s2 in
+        if Int.equal r 0 then assert (Bool.equal unsigned1 unsigned2) ;
+        r
 
 
-  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+  type 'res eval = t -> BoundEnd.t -> 'res AbstractDomain.Types.bottom_lifted
 
   let equal = [%compare.equal: t]
 
-  let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
+  let paths_equal s1 s2 =
+    match (s1, s2) with
+    | OneValue _, BoundEnd _ | BoundEnd _, OneValue _ ->
+        false
+    | OneValue {path= path1}, OneValue {path= path2}
+    | BoundEnd {path= path1}, BoundEnd {path= path2} ->
+        SymbolPath.equal path1 path2
+
+
+  let make_onevalue : unsigned:bool -> SymbolPath.t -> t =
+   fun ~unsigned path -> OneValue {unsigned; path}
+
 
-  let make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t =
-   fun ~unsigned path bound_end -> {unsigned; path; bound_end}
+  let make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t =
+   fun bound_end ~unsigned path -> BoundEnd {unsigned; path; bound_end}
 
 
   let pp : F.formatter -> t -> unit =
    fun fmt s ->
-    SymbolPath.pp fmt s.path ;
-    if Config.developer_mode then Format.fprintf fmt ".%s" (BoundEnd.to_string s.bound_end) ;
-    if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if s.unsigned then 'u' else 's')
+    match s with
+    | OneValue {unsigned; path} | BoundEnd {unsigned; path} ->
+        SymbolPath.pp fmt path ;
+        ( if Config.developer_mode then
+          match s with
+          | BoundEnd {bound_end} ->
+              Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end)
+          | OneValue _ ->
+              () ) ;
+        if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if unsigned then 'u' else 's')
 
 
   let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
 
-  let is_unsigned {unsigned} = unsigned
+  let is_unsigned : t -> bool = function OneValue {unsigned} | BoundEnd {unsigned} -> unsigned
 
-  let path {path} = path
+  let path = function OneValue {path} | BoundEnd {path} -> path
 
-  let bound_end {bound_end} = bound_end
+  let assert_bound_end s be =
+    match s with OneValue _ -> () | BoundEnd {bound_end} -> assert (BoundEnd.equal be bound_end)
 end
 
 module SymbolSet = struct
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index 63f4819dd..430761cfa 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/infer/src/bufferoverrun/symb.mli
@@ -54,13 +54,15 @@ module SymbolPath : sig
 
   val represents_multiple_values : partial -> bool
 
+  val represents_multiple_values_sound : partial -> bool
+
   val represents_callsite_sound_partial : partial -> bool
 end
 
 module Symbol : sig
   type t
 
-  type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
+  type 'res eval = t -> BoundEnd.t -> 'res AbstractDomain.Types.bottom_lifted
 
   val compare : t -> t -> int
 
@@ -74,9 +76,11 @@ module Symbol : sig
 
   val path : t -> SymbolPath.t
 
-  val bound_end : t -> BoundEnd.t
+  val assert_bound_end : t -> BoundEnd.t -> unit
+
+  val make_onevalue : unsigned:bool -> SymbolPath.t -> t
 
-  val make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t
+  val make_boundend : BoundEnd.t -> unsigned:bool -> SymbolPath.t -> t
 end
 
 module SymbolSet : sig
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
index d7a410489..9519e9cc5 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c
@@ -38,6 +38,11 @@ void l1_symbolic_overrun_Bad(int i) {
   }
 }
 
+void l1_symbolic_overrun2_Bad(int n) {
+  int a[n];
+  a[n] = 0;
+}
+
 void l1_symbolic_underrun_Bad(int i) {
   int a[10];
   if (i < 0) {
@@ -45,6 +50,22 @@ void l1_symbolic_underrun_Bad(int i) {
   }
 }
 
+int less_than(int i, int n) { return i < n; }
+
+void l1_symbolic_widened_Bad(int n) {
+  int a[n];
+  for (int i = n; less_than(i, 2 * n); i++) {
+    a[i] = 0;
+  }
+}
+
+void l1_symbolic_widened_Good_FP(int n) {
+  int a[n];
+  for (int i = n; less_than(i, n); i++) {
+    a[i] = 0;
+  }
+}
+
 void l2_concrete_overrun_Bad() {
   int a[10];
   a[zero_or_ten(1)] = 0;
@@ -65,9 +86,9 @@ void l2_concrete_no_underrun_Good_FP() {
   a[zero_or_ten(1) - 1] = 0;
 }
 
-void l2_symbolic_overrun_Bad(int n) {
-  int a[n];
-  a[n] = 0;
+void l2_symbolic_overrun_Bad(int* n) {
+  int a[*n];
+  a[*n] = 0;
 }
 
 void l2_symbolic_no_overrun_Good(int n) {
@@ -97,8 +118,6 @@ void l3_concrete_no_underrun_Good_FP() {
   a[zero_or_ten(1) - 1] = 0;
 }
 
-int less_than(int i, int n) { return i < n; }
-
 void l4_widened_overrun_Bad() {
   int a[10];
   for (int i = 0; less_than(i, 11); i++) {
@@ -120,25 +139,30 @@ void l5_external_Warn_Bad() {
   a[unknown_function()] = 0;
 }
 
-void s2_symbolic_widened_Bad(int n) {
-  int a[n];
-  for (int i = n; less_than(i, 2 * n); i++) {
+void s2_symbolic_widened_Bad(int* n) {
+  int a[*n];
+  for (int i = *n; less_than(i, 2 * *n); i++) {
     a[i] = 0;
   }
 }
 
-void s2_symbolic_widened_Good_FP(int n) {
-  int a[n];
-  for (int i = n; less_than(i, n); i++) {
+void s2_symbolic_widened_Good_FP(int* n) {
+  int a[*n];
+  for (int i = *n; less_than(i, *n); i++) {
     a[i] = 0;
   }
 }
 
 // Do not report as it was already reported in the callee with the same issue
 // type
-void call_s2_symbolic_widened_Silenced(int m) { s2_symbolic_widened_Bad(m); }
+void FP_call_s2_symbolic_widened_Silenced(int* m) {
+  s2_symbolic_widened_Bad(m);
+}
 
-void l1_call_to_s2_symbolic_widened_Bad() { s2_symbolic_widened_Bad(1); }
+void l1_call_to_s2_symbolic_widened_Bad() {
+  int x = 1;
+  s2_symbolic_widened_Bad(&x);
+}
 
 void may_underrun_symbolic_Nowarn_Good(int n) {
   int a[n];
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
index a8574f09d..d5cc360a2 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
@@ -57,7 +57,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Bad, 3, BUFFER_OVERRU
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 15] Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/array_content.c, weak_update_malloc_Good_FP, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
-codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
+codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: 3⋅len + 1 Size: 3⋅len + 1]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `y.f[*]`,<Length trace>,Array declaration,Array access: Offset: [min(20, y.f[*]), max(20, y.f[*])] Size: 10]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f[*]`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
 codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
@@ -100,7 +100,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_call_access_index_4_on_S3_Ba
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
+codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
@@ -132,21 +132,24 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, call_to_alloc_may_be_big2_is_big_Ba
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, call_two_safety_conditions_l1_and_l2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: [9, 11] Size: 10 by call to `two_safety_conditions` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, deduplicate_issues_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: [10, +oo] Size: 10]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [1, +oo] Size: 1 by call to `s2_symbolic_widened_Bad` ]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_call_to_s2_symbolic_widened_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `*n`,Assignment,Binary operation: ([1, +oo] + 1):signed32 by call to `s2_symbolic_widened_Bad` ]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: n Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [max(10, i), i] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_underrun_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `i`,<Length trace>,Array declaration,Array access: Offset: [i, min(-1, i)] Size: 10]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: unknown_function,Binary operation: ([-oo, +oo] × 10):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_unknown_function_Bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,Assignment,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: n Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: *n Size: *n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]]
@@ -156,13 +159,12 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_no_overrun_Good_FP, 3, B
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l4_widened_overrun_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, +oo] Size: 10]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, l5_external_Warn_Bad, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: unknown_function,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
-codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: [n, +oo] Size: n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Bad, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
+codetoanalyze/c/bufferoverrun/issue_kinds.c, s2_symbolic_widened_Good_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [<Offset trace>,Parameter `*n`,Assignment,<Length trace>,Parameter `*n`,Array declaration,Array access: Offset: [*n, +oo] Size: *n]
 codetoanalyze/c/bufferoverrun/issue_kinds.c, zero_to_infty, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/minmax.c, exact_min_plus_min_plus_min_UNDERRUN, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-19+min(0, x), -1] Size: 1]
 codetoanalyze/c/bufferoverrun/minmax.c, underapprox_min_minus_min_linear_CAF, 6, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/models.c, call_memcpy_len2_Good_FP, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: unknown,Assignment,Call,<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset added: [0, +oo] Size: [0, +oo] by call to `memcpy_len` ]
 codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACHABLE_CODE, no_bucket, ERROR, [Here]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 255] Size: 255]
 codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 256] Size: 256]
@@ -197,19 +199,22 @@ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label,
 codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `x`,<Length trace>,Parameter `*p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
-codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
+codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5]
 codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_eq_CAF` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ]
-codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
+codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne_CAT` ]
 codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
+codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_exp2_CAF, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_exp_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_ge_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_gt_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c
index 5fe1f14a0..13f707e72 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c
@@ -97,19 +97,19 @@ void memcpy_good4() {
   memcpy(dst, src, sizeof(dst));
 }
 
-void memcpy_len(size_t len) {
+void memcpy_len_Good(size_t len) {
   char dst[len];
   char src[len];
   memcpy(dst, src, len);
 }
 
-void call_memcpy_len1_Good() { memcpy_len(40); }
+void call_memcpy_len1_Good() { memcpy_len_Good(40); }
 
 extern size_t unknown_uint();
 
-void call_memcpy_len2_Good_FP() {
+void call_memcpy_len2_Good() {
   size_t x = unknown();
-  memcpy_len(x);
+  memcpy_len_Good(x);
 }
 
 void memmove_bad1() {
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c
index 7b61735bd..6ba2478af 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c
@@ -36,17 +36,26 @@ void call_pointer_arith3_Bad() {
   pointer_arith3(p, 100);
 }
 
+void pointer_arith4_Bad(int x) {
+  int len = 5;
+  char p[5];
+  (p + x)[10 - x] = 0;
+}
+
 /* It is better to raise an alarm here, rather than returning a safety
    condition, since the buffer overrun occurs always without regard to
    the input x.  Using symbols for variables, not only for bounds,
    would help in this case. */
-void FN_pointer_arith4_Bad(int x) {
+void FN_pointer_arith4_Bad(int* x) {
   int len = 5;
   char p[5];
-  (p + x)[10 - x] = 0;
+  (p + *x)[10 - *x] = 0;
 }
 
-void call_pointer_arith4_Bad() { FN_pointer_arith4_Bad(100); }
+void call_pointer_arith4_Bad() {
+  int x = 100;
+  FN_pointer_arith4_Bad(&x);
+}
 
 #include <stdio.h>
 #include <stdlib.h>
diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
index 2aee13274..803deb189 100644
--- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
+++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c
@@ -98,45 +98,53 @@ void prune_alias_exp_Ok(int x) {
   }
 }
 
-void FP_prune_alias_exp_Ok(int x) {
+void prune_alias_exp2_CAF(int x) {
   int a[1];
 
-  if (x + 1 != 1 + x) {
+  if (x + 1 != 1 + x) { // Condition always false
+    a[1] = 0;
+  }
+}
+
+void FP_prune_alias_exp_Ok(int* x) {
+  int a[1];
+
+  if (*x + 1 != 1 + *x) {
     a[1] = 0;
   }
 }
 
 #include <stdlib.h>
 
-void prune_arrblk_ne(int* x) {
+void prune_arrblk_ne_CAT(int* x) {
   int* y = x + 10;
 
-  if (x != y) {
+  if (x != y) { // always true
     x[5] = 1;
   }
 }
 
 void call_prune_arrblk_ne_Ok() {
   int* x = (int*)malloc(sizeof(int) * 10);
-  prune_arrblk_ne(x);
+  prune_arrblk_ne_CAT(x);
 }
 
 void call_prune_arrblk_ne_Bad() {
   int* x = (int*)malloc(sizeof(int) * 5);
-  prune_arrblk_ne(x);
+  prune_arrblk_ne_CAT(x);
 }
 
-void prune_arrblk_eq(int* x) {
+void prune_arrblk_eq_CAF(int* x) {
   int* y = x + 10;
 
-  if (x == y) {
+  if (x == y) { // always false
     x[5] = 1; /* unreachable */
   }
 }
 
-void call_prune_arrblk_eq_Ok() {
+void FP_call_prune_arrblk_eq_Ok() {
   int* x = (int*)malloc(sizeof(int) * 5);
-  prune_arrblk_eq(x);
+  prune_arrblk_eq_CAF(x);
 }
 
 void prune_minmax1_Ok(unsigned int x, unsigned int y) {
diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp
index b164d38a7..e139d71cb 100644
--- a/infer/tests/codetoanalyze/c/performance/issues.exp
+++ b/infer/tests/codetoanalyze/c/performance/issues.exp
@@ -1,17 +1,17 @@
-codetoanalyze/c/performance/break.c, break_constant, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), 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.ub + 2 ⋅ (1+max(0, p.ub)), 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.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/break.c, break_loop_with_t, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), 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]
+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, 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, 3, 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, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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_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_loop_with_t, 3, 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, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
 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.ub + 4 ⋅ (1+max(0, m.ub)), 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.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, compound_while, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 3 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), 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]
+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, 4, 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, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 3 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
 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]
@@ -32,10 +32,10 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an
 codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_and, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3532, degree = 0]
 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, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ p.ub + 4 ⋅ (1+max(0, p.ub)), degree = 1]
+codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, 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, 4, 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, 10, 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, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1]
 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]
@@ -47,13 +47,13 @@ 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, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1207, degree = 0]
 codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1209, degree = 0]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), degree = 1]
-codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 ⋅ k.ub + 2 ⋅ (1+max(0, k.ub)), 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]
+codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, 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, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 10 ⋅ k + 2 ⋅ (1+max(0, k)), degree = 1]
 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.lb + 20), degree = 1]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ (-m.lb + 20), degree = 1]
-codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 ⋅ (-m.lb + 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]
+codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, 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, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 6 ⋅ (-m + 20), degree = 1]
 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, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, if_bad_loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 235, degree = 0]
@@ -115,26 +115,26 @@ 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, no_bucket, ERROR, [with estimated cost 551, degree = 0]
 codetoanalyze/c/performance/cost_test_deps.c, two_loops, 10, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 553, 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.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ (m.ub - 1) × m.ub + 8 ⋅ m.ub + 2 ⋅ m.ub × (max(1, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_m2_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 8 ⋅ m.ub + 6 ⋅ m.ub² + 2 ⋅ m.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 2]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/instantiate.c, do_n_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 3 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), 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.ub + 2 ⋅ (1+max(0, n.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, do_k_times_array, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 6 ⋅ n.ub + 2 ⋅ (1+max(0, n.ub)), 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.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), degree = 2]
-codetoanalyze/c/performance/invariant.c, do_n_m_times_nested, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 6 ⋅ n.ub + 3 ⋅ n.ub × m.ub + 2 ⋅ n.ub × (1+max(0, m.ub)) + 2 ⋅ (1+max(0, n.ub)), 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.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), degree = 1]
-codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p.ub + 2 ⋅ (1+max(0, p.ub)), 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]
+codetoanalyze/c/performance/instantiate.c, do_half_m2_times, 2, 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_m2_times, 2, 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/instantiate.c, do_n_times, 2, 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, 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_k_times_array, 4, 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, 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, do_n_m_times_nested, 4, 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, do_n_m_times_nested, 4, 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, do_n_m_times_nested, 4, 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/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/invariant.c, two_loops_nested_invariant, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
+codetoanalyze/c/performance/invariant.c, two_loops_nested_invariant, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 24 ⋅ p + 2 ⋅ (1+max(0, p)), degree = 1]
 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, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004, degree = 0]
 codetoanalyze/c/performance/jump_inside_loop.c, jump_inside_loop, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2004, degree = 0]
@@ -160,9 +160,9 @@ codetoanalyze/c/performance/loops.c, larger_state_FN, 3, EXPENSIVE_EXECUTION_TIM
 codetoanalyze/c/performance/loops.c, larger_state_FN, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
 codetoanalyze/c/performance/loops.c, larger_state_FN, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1006, degree = 0]
 codetoanalyze/c/performance/loops.c, larger_state_FN, 7, 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 4 + 4 ⋅ x.ub + 2 ⋅ (1+max(0, x.ub)), 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.ub + 2 ⋅ (1+max(0, x.ub)), 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.ub + 2 ⋅ (1+max(0, x.ub)), 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]
+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 4 + 4 ⋅ x + 2 ⋅ (1+max(0, x)), degree = 1]
 codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
 codetoanalyze/c/performance/purity.c, loop, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
 codetoanalyze/c/performance/purity.c, loop, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7006, degree = 0]
@@ -176,15 +176,15 @@ codetoanalyze/c/performance/switch_continue.c, test_switch, 19, EXPENSIVE_EXECUT
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/c/performance/switch_continue.c, unroll_loop_FP, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 ⋅ m.ub + 4 ⋅ (1+max(0, m.ub)), 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.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), 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, 4, 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, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ m + 4 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 12 ⋅ m + 4 ⋅ (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/two_loops_symbolic.c, two_loops_symb_diff, 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, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), degree = 1]
+codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ k + 6 ⋅ m + 2 ⋅ (1+max(0, k)) + 2 ⋅ (1+max(0, m)), degree = 1]
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
index 1af2b5475..3bbd85f02 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
@@ -1,2 +1,2 @@
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
-codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy.ub - 1] × d.cci[*].s):signed32]
+codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 8f07497fa..10a83e2f9 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -1,9 +1,9 @@
 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 3 + 15 ⋅ length.ub, 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.ub, degree = 1]
-codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ mag.length.ub, 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.ub, 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]
+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 3 + 15 ⋅ length, degree = 1]
+codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 2, 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 7 + 5 ⋅ mag.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/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
@@ -25,49 +25,49 @@ 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.ub × log(list.length.ub), 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 7 + 5 ⋅ list.length.ub, degree = 1]
-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.ub, 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.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-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 6 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-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]
+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(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 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.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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.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_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
-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.ub - 1) + 4 ⋅ list1.length.ub, 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 9 + 13 ⋅ (list1.length.ub - 1) + 4 ⋅ list1.length.ub, 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 9 + 5 ⋅ list.length.ub, 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.ub, 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.ub - 1) + 4 ⋅ list.length.ub, 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 6 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, 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 6 + 9 ⋅ (list.length.ub - 1) + 4 ⋅ list.length.ub, 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.ub - 1) + 4 ⋅ list.length.ub, degree = 1]
-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.ub × log(list.length.ub), 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.ub, 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 3 + 7 ⋅ p.ub, 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.ub, 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 3 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-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.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI.ub + 3 ⋅ maxI.ub × (min(12, maxJ.ub)) + 5 ⋅ maxI.ub × (12-max(0, maxJ.lb)) + 5 ⋅ (min(11, maxI.ub)) × (min(11, maxJ.ub)), degree = 2]
-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.ub, 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.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, degree = 2]
-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 6 + 21 ⋅ (list.length.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, 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.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, 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 6 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, 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.ub - 1) + 4 ⋅ mSubscribers.length.ub, 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.ub - 1) + 4 ⋅ mSubscribers.length.ub, 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 6 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, 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.ub + 5 ⋅ size.ub × list.length.ub, degree = 2]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 17 ⋅ size.ub + 5 ⋅ size.ub × list.length.ub, 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 6 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-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.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 15 ⋅ (list1.length.ub - 1) + 33 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) + 10 ⋅ (list1.length.ub - 1) × (list2.length.ub - 1) × list1.length.ub + 4 ⋅ (list1.length.ub - 1) × list2.length.ub + 4 ⋅ list1.length.ub, degree = 3]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, 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.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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.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_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 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_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 9 + 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_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 12 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 4, 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.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (list.length - 1) + 4 ⋅ list.length, degree = 1]
+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_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 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 3 + 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/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/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 5, 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/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 7, 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/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_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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 7 + 5 ⋅ list.length, degree = 1]
+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 6 + 21 ⋅ (mSubscribers.length - 1) + 4 ⋅ mSubscribers.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.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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 3 + 17 ⋅ size + 5 ⋅ size × list.length, degree = 2]
+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.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 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.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 2, 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.nested_iterator_qubic(int,CollectionTest$MyCollection,CollectionTest$MyCollection):void, 4, 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/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.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
-codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), 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]
+codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.compound_while(int):int, 4, 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.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]
@@ -79,8 +79,8 @@ codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Con
 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/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0]
 codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 4, 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.ub, 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 3 + 13 ⋅ k.ub, 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 3 + 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]
 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.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1203, 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]
@@ -115,24 +115,24 @@ 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, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0]
 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 546, 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 3 + 6 ⋅ test.a.ub, 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.ub, 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.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), degree = 1]
-codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 ⋅ (k.ub - 1) + 4 ⋅ (max(1, k.ub)), 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]
+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 3 + 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/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1]
+codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1]
 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.ub + 4 ⋅ (items.length.ub + 1), 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 3 + 5 ⋅ items.length.ub + 4 ⋅ (items.length.ub + 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.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), degree = 2]
-codetoanalyze/java/performance/Invariant.java, Invariant.local_not_invariant_FP(int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 ⋅ (size.ub + 5) + 7 ⋅ (size.ub + 5) × (5+min(1, size.ub)) + 4 ⋅ (5+min(0, size.ub)), 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 9 + 6 ⋅ (size.ub + 20), degree = 1]
-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.ub + 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.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
-codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
-codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.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]
+codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 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 4 + 12 ⋅ (size + 5) + 7 ⋅ (size + 5) × (5+min(1, size)) + 4 ⋅ (5+min(0, size)), degree = 2]
+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.local_not_invariant_FP(int):void, 5, 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 9 + 6 ⋅ (size + 20), degree = 1]
+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 2 + 12 ⋅ (parts.length - 1) + 4 ⋅ parts.length, 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/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 2, 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,boolean):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ String.toCharArray().length.ub, degree = 1]
@@ -160,22 +160,22 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 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.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, 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 3 + 29 ⋅ (length.ub - 1), degree = 1]
-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.ub - 1), degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 ⋅ (length.ub - 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 4 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 29 ⋅ (length - 1), degree = 1]
+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.dumb0(long[],int):void, 2, 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 4 + 71 ⋅ (length - 1)² + 8 ⋅ length, degree = 2]
+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.dumbSort(long[],long[],int):void, 2, 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.dumbSort(long[],long[],int):void, 3, 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.dumbSort(long[],long[],int):void, 5, 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.dumbSort(long[],long[],int):void, 7, 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.dumbSort(long[],long[],int):void, 9, 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.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 14 + 33 ⋅ x.length.ub, 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 13 + 33 ⋅ x.length.ub, degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, 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 14 + 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 13 + 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, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 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, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length, degree = 1]
 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.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]