diff --git a/infer/src/IR/IntLit.ml b/infer/src/IR/IntLit.ml
index 33206dc21..7bff07bc8 100644
--- a/infer/src/IR/IntLit.ml
+++ b/infer/src/IR/IntLit.ml
@@ -148,6 +148,8 @@ let shift_right intlit1 {i= i2} =
       lift1 (fun i -> Z.shift_right i i2) intlit1
 
 
+let min i1 i2 = if leq i1 i2 then i1 else i2
+
 let pp f intlit = if isnull intlit then F.pp_print_string f "null" else Z.pp_print f intlit.i
 
 let to_string i = F.asprintf "%a" pp i
diff --git a/infer/src/IR/IntLit.mli b/infer/src/IR/IntLit.mli
index 6686fff83..b239d775d 100644
--- a/infer/src/IR/IntLit.mli
+++ b/infer/src/IR/IntLit.mli
@@ -89,6 +89,8 @@ val shift_right : t -> t -> t
 
 val sub : t -> t -> t
 
+val min : t -> t -> t
+
 val to_int : t -> int option
 
 val to_int_exn : t -> int
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index fdda45b9e..5adadc5ba 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -817,6 +817,19 @@ module MemPure = struct
 end
 
 module AliasTarget = struct
+  (* [Eq]: The value of alias target is exactly the same to the alias key.
+
+     [Le]: The value of alias target is less than or equal to the alias key.  For example, if there
+     is an alias between [%r] and [size(x)+i] with the [Le] type, which means [size(x)+i <= %r]. *)
+  type alias_typ = Eq | Le [@@deriving compare]
+
+  let alias_typ_pp fmt = function
+    | Eq ->
+        F.pp_print_string fmt "="
+    | Le ->
+        F.pp_print_string fmt ">="
+
+
   (* Relations between values of logical variables(registers) and program variables
 
    "Simple relation": Since Sil distinguishes logical and program variables, we need a relation for
@@ -839,7 +852,7 @@ module AliasTarget = struct
   type t =
     | Simple of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Empty of Loc.t
-    | Size of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
+    | Size of {alias_typ: alias_typ; l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Fgets of Loc.t
     | Top
   [@@deriving compare]
@@ -858,8 +871,9 @@ module AliasTarget = struct
           F.fprintf fmt "%t%a=%a%a" pp_key pp_java_tmp java_tmp Loc.pp l pp_intlit i
       | Empty l ->
           F.fprintf fmt "%t=empty(%a)" pp_key Loc.pp l
-      | Size {l; i; java_tmp} ->
-          F.fprintf fmt "%t%a=size(%a)%a" pp_key pp_java_tmp java_tmp Loc.pp l pp_intlit i
+      | Size {alias_typ; l; i; java_tmp} ->
+          F.fprintf fmt "%t%a%asize(%a)%a" pp_key pp_java_tmp java_tmp alias_typ_pp alias_typ
+            Loc.pp l pp_intlit i
       | Fgets l ->
           F.fprintf fmt "%t=fgets(%a)" pp_key Loc.pp l
       | Top ->
@@ -888,27 +902,60 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Simple {l; i; java_tmp})
     | Empty l ->
         Option.map (f l) ~f:(fun l -> Empty l)
-    | Size {l; i; java_tmp} ->
+    | Size {alias_typ; l; i; java_tmp} ->
         let java_tmp = Option.bind java_tmp ~f in
-        Option.map (f l) ~f:(fun l -> Size {l; i; java_tmp})
+        Option.map (f l) ~f:(fun l -> Size {alias_typ; l; i; java_tmp})
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
     | Top ->
         Some Top
 
 
-  let ( <= ) ~lhs ~rhs = equal lhs rhs
+  let ( <= ) ~lhs ~rhs =
+    equal lhs rhs
+    ||
+    match (lhs, rhs) with
+    | ( Size {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
+      , Size {alias_typ= Le; l= l2; i= i2; java_tmp= java_tmp2} ) ->
+        (* (a=size(l)+2) <= (a>=size(l)+1)  *)
+        (* (a>=size(l)+2) <= (a>=size(l)+1)  *)
+        Loc.equal l1 l2 && IntLit.geq i1 i2 && Option.equal Loc.equal java_tmp1 java_tmp2
+    | _, _ ->
+        false
 
-  let join x y = if equal x y then x else Top
 
-  let widen ~prev ~next ~num_iters:_ = join prev next
+  let join x y =
+    if equal x y then x
+    else
+      match (x, y) with
+      | ( Size {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
+        , Size {alias_typ= _; l= l2; i= i2; java_tmp= java_tmp2} )
+        when Loc.equal l1 l2 && Option.equal Loc.equal java_tmp1 java_tmp2 ->
+          (* (a=size(l)+1) join (a=size(l)+2) is (a>=size(l)+1) *)
+          (* (a=size(l)+1) join (a>=size(l)+2) is (a>=size(l)+1) *)
+          Size {alias_typ= Le; l= l1; i= IntLit.min i1 i2; java_tmp= java_tmp1}
+      | _, _ ->
+          Top
+
+
+  let widen ~prev ~next ~num_iters:_ =
+    if equal prev next then prev
+    else
+      match (prev, next) with
+      | Size {alias_typ= Eq}, Size {alias_typ= _} ->
+          join prev next
+      | Size {alias_typ= Le; i= i1}, Size {alias_typ= _; i= i2} when IntLit.eq i1 i2 ->
+          join prev next
+      | _, _ ->
+          Top
+
 
   let is_unknown x = PowLoc.exists Loc.is_unknown (get_locs x)
 
   let incr_size_alias loc x =
     match x with
-    | Size {l; i} when Loc.equal l loc ->
-        Size {l; i= IntLit.(add i minus_one); java_tmp= None}
+    | Size {alias_typ; l; i} when Loc.equal l loc ->
+        Size {alias_typ; l; i= IntLit.(add i minus_one); java_tmp= None}
     | _ ->
         x
 end
@@ -1001,15 +1048,17 @@ module AliasMap = struct
 
 
   let add_zero_size_alias ~size ~arr x =
-    add (Key.of_loc size) (AliasTarget.Size {l= arr; i= IntLit.zero; java_tmp= None}) x
+    add (Key.of_loc size)
+      (AliasTarget.Size {alias_typ= Eq; l= arr; i= IntLit.zero; java_tmp= None})
+      x
 
 
   let incr_size_alias loc = map (AliasTarget.incr_size_alias loc)
 
   let store_n ~prev loc id n x =
     match find_id id prev with
-    | Some (AliasTarget.Size {l; i}) ->
-        add (Key.of_loc loc) (AliasTarget.Size {l; i= IntLit.add i n; java_tmp= None}) x
+    | Some (AliasTarget.Size {alias_typ; l; i}) ->
+        add (Key.of_loc loc) (AliasTarget.Size {alias_typ; l; i= IntLit.add i n; java_tmp= None}) x
     | _ ->
         x
 end
@@ -1096,7 +1145,8 @@ module Alias = struct
 
 
   let add_empty_size_alias : Loc.t -> PowLoc.t -> t -> t =
-   fun loc arr_locs a ->
+   fun loc arr_locs prev ->
+    let a = lift_map (AliasMap.forget loc) prev in
     match PowLoc.is_singleton_or_more arr_locs with
     | IContainer.Singleton arr_loc ->
         lift_map (AliasMap.add_zero_size_alias ~size:loc ~arr:arr_loc) a
@@ -1606,11 +1656,11 @@ module MemReach = struct
         None
 
 
-  let find_size_alias : Ident.t -> _ t0 -> (Loc.t * Loc.t option) option =
+  let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) option =
    fun k m ->
     match Alias.find_id k m.alias with
-    | Some (AliasTarget.Size {l; java_tmp}) ->
-        Some (l, java_tmp)
+    | Some (AliasTarget.Size {alias_typ; l; java_tmp}) ->
+        Some (alias_typ, l, java_tmp)
     | _ ->
         None
 
@@ -1933,7 +1983,7 @@ module Mem = struct
    fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k)
 
 
-  let find_size_alias : Ident.t -> _ t0 -> (Loc.t * Loc.t option) option =
+  let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) option =
    fun k -> f_lift_default ~default:None (MemReach.find_size_alias k)
 
 
@@ -1954,7 +2004,8 @@ module Mem = struct
 
 
   let load_size_alias : Ident.t -> Loc.t -> t -> t =
-   fun id loc -> load_alias id (AliasTarget.Size {l= loc; i= IntLit.zero; java_tmp= None})
+   fun id loc ->
+    load_alias id (AliasTarget.Size {alias_typ= Eq; l= loc; i= IntLit.zero; java_tmp= None})
 
 
   let store_simple_alias : Loc.t -> Exp.t -> t -> t =
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 57860eade..b1189f9a0 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -556,7 +556,8 @@ module Prune = struct
 
 
   let gen_prune_alias_functions ~prune_alias_core integer_type_widths comp x e astate =
-    let val_prune =
+    (* [val_prune_eq] is applied when the alias type is [AliasTarget.Eq]. *)
+    let val_prune_eq =
       match comp with
       | Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge ->
           Val.prune_comp comp
@@ -567,19 +568,37 @@ module Prune = struct
       | _ ->
           assert false
     in
+    (* [val_prune_le] is applied when the alias type is [AliasTarget.Le]. *)
+    let val_prune_le =
+      match comp with
+      | Binop.Lt ->
+          (* when [alias_target <= alias_key < e], prune [alias_target] with [alias_target < e] *)
+          Some (Val.prune_comp comp)
+      | Binop.Le | Binop.Eq ->
+          (* when [alias_target <= alias_key = e] or [alias_target <= alias_key <= e], prune
+             [alias_target] with [alias_target <= e] *)
+          Some (Val.prune_comp Binop.Le)
+      | Binop.Ne | Binop.Gt | Binop.Ge ->
+          (* when [alias_target <= alias_key != e], [alias_target <= alias_key > e] or [alias_target
+             <= alias_key >= e], no prune *)
+          None
+      | _ ->
+          assert false
+    in
     let make_pruning_exp = PruningExp.make comp in
-    prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e astate
+    prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e astate
 
 
   let prune_simple_alias =
-    let prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e ({mem} as astate) =
+    let prune_alias_core ~val_prune_eq ~val_prune_le:_ ~make_pruning_exp integer_type_widths x e
+        ({mem} as astate) =
       Option.value_map (Mem.find_simple_alias x mem) ~default:astate ~f:(fun (lv, opt_i) ->
           let lhs = Mem.find lv mem in
           let rhs =
             let v' = eval integer_type_widths e mem in
             Option.value_map opt_i ~default:v' ~f:(fun i -> Val.minus_a v' (Val.of_int_lit i))
           in
-          let v = val_prune lhs rhs in
+          let v = val_prune_eq lhs rhs in
           let pruning_exp = make_pruning_exp ~lhs ~rhs in
           update_mem_in_prune lv v ~pruning_exp astate )
     in
@@ -587,20 +606,36 @@ module Prune = struct
 
 
   let prune_size_alias =
-    let prune_alias_core ~val_prune ~make_pruning_exp integer_type_widths x e ({mem} as astate) =
-      Option.value_map (Mem.find_size_alias x mem) ~default:astate ~f:(fun (lv, java_tmp) ->
+    let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e
+        ({mem} as astate) =
+      Option.value_map (Mem.find_size_alias x mem) ~default:astate
+        ~f:(fun (alias_typ, lv, java_tmp) ->
           let array_v = Mem.find lv mem in
           let size =
             Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv
             |> Val.set_itv_updated_by_addition
           in
           let rhs = eval integer_type_widths e mem in
-          let size' = val_prune size rhs in
-          let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in
-          let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in
-          let astate = update_mem_in_prune lv array_v' ~pruning_exp astate in
-          Option.value_map java_tmp ~default:astate ~f:(fun java_tmp ->
-              update_mem_in_prune java_tmp size' ~pruning_exp astate ) )
+          let prune_target val_prune astate =
+            let size' = val_prune size rhs in
+            let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in
+            let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in
+            (update_mem_in_prune lv array_v' ~pruning_exp astate, size', pruning_exp)
+          in
+          match alias_typ with
+          | AliasTarget.Eq ->
+              let astate, size', pruning_exp = prune_target val_prune_eq astate in
+              Option.value_map java_tmp ~default:astate ~f:(fun java_tmp ->
+                  update_mem_in_prune java_tmp size' ~pruning_exp astate )
+          | AliasTarget.Le ->
+              let astate =
+                Option.value_map val_prune_le ~default:astate ~f:(fun val_prune_le ->
+                    prune_target val_prune_le astate |> fun (astate, _, _) -> astate )
+              in
+              Option.value_map java_tmp ~default:astate ~f:(fun java_tmp ->
+                  let v = val_prune_eq (Mem.find java_tmp mem) rhs in
+                  let pruning_exp = make_pruning_exp ~lhs:v ~rhs in
+                  update_mem_in_prune java_tmp v ~pruning_exp astate ) )
     in
     gen_prune_alias_functions ~prune_alias_core
 
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java
index bdfa275af..37bf151ec 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java
@@ -49,4 +49,28 @@ class ArrayListTest {
     }
     int j = a.get(b.size() + 1);
   }
+
+  boolean unknown_bool;
+
+  void add_in_loop_by_param2_ok(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    for (int i = 0; i < b.size(); i++) {
+      if (unknown_bool) {
+        a.add(0);
+      }
+    } // a.size should be [0, b.size]
+    if (a.size() > 0) {
+      int j = b.get(a.size() - 1);
+    }
+  }
+
+  void add_in_loop_by_param2_bad(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    for (int i = 0; i < b.size(); i++) {
+      if (unknown_bool) {
+        a.add(0);
+      }
+    } // a.size should be [0, b.size]
+    int j = b.get(a.size());
+  }
 }
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
index 22f6152ee..5e069dd4c 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
@@ -8,6 +8,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.prune_assign_exp_Bad():void, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 4] Size: 3]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Assignment,Array declaration,Array access: Offset: [0, b.length] Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
 codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java
index 08f853f04..93b357324 100644
--- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java
+++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java
@@ -42,9 +42,8 @@ public class ArrayListTest {
     list.add(4, 666);
   }
 
-  // we can't set the size of the list to 10 because it depends on how
-  // many times the loop is executed.Should be fixed once we have
-  // relational domain working.
+  // We can set the size of the list to 10.  The reason of FP is that the widened [i] value at the
+  // second loop is failed to be narrowed precisely.
   public void arraylist_add_in_loop_FP() {
     ArrayList<Integer> list = new ArrayList<Integer>();
     for (int i = 0; i < 10; ++i) {
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 95c878103..c260b85a0 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -18,36 +18,36 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void,
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 883, O(1), degree = 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset added: 5 Size: 4]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 53]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 52]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: 1 Size: 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset added: -1 Size: 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 2 Size: 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Array access: Offset: 1 Size: 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 164]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 163]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
 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.boolean_control_var_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 19 ⋅ this.arr.length + 4 ⋅ (this.arr.length + 1), O(this.arr.length), degree = 1,{this.arr.length + 1},Loop at line 295,{this.arr.length},Loop at line 295]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.boolean_control_var_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 19 ⋅ this.arr.length + 4 ⋅ (this.arr.length + 1), O(this.arr.length), degree = 1,{this.arr.length + 1},Loop at line 294,{this.arr.length},Loop at line 294]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 245,{l.length + list.length},Loop at line 245]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 252,{l.length + list.length},Loop at line 252]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 227,{list.length},Loop at line 227]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 238,{list.length + 4},Loop at line 238]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 244,{l.length + list.length},Loop at line 244]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 251,{l.length + list.length},Loop at line 251]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 226,{list.length},Loop at line 226]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 237,{list.length + 4},Loop at line 237]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 14]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 193,{list.length + 1},Loop at line 193,{11-max(10, list.elements)},Loop at line 193,{list.length},Loop at line 193]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ list1.length + 3 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 184,{list1.length},Loop at line 184]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 192,{list.length + 1},Loop at line 192,{11-max(10, list.elements)},Loop at line 192,{list.length},Loop at line 192]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ list1.length + 3 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 183,{list1.length},Loop at line 183]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 19]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 176,{list.length},Loop at line 176]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 170,{list.length},Loop at line 170]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.json_array_constructor_linear(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ arr.length + 3 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 272,{arr.length},Loop at line 272]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.linear(int,java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 9 ⋅ (-i + a.length + 1), O((-i + a.length)), degree = 1,{-i + a.length + 1},Loop at line 279]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 175,{list.length},Loop at line 175]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 169,{list.length},Loop at line 169]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.json_array_constructor_linear(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ arr.length + 3 ⋅ (arr.length + 1), O(arr.length), degree = 1,{arr.length + 1},Loop at line 271,{arr.length},Loop at line 271]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.linear(int,java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 9 ⋅ (-i + a.length + 1), O((-i + a.length)), degree = 1,{-i + a.length + 1},Loop at line 278]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java.util.ArrayList):Person, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length, O(people.length), degree = 1,{people.length},Modeled call to Collections.max]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ this.list.length + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 216,{this.list.length},Loop at line 216]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ this.list.length + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 215,{this.list.length},Loop at line 215]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), O(people.length × log(people.length)), degree = 1 + 1⋅log,{people.length},Modeled call to Collections.sort,{people.length},Modeled call to Collections.sort]
 codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, O(p), degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12]