diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index f6c8fbcf1..e441004aa 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -257,6 +257,8 @@ module Loc = struct
         false
 
 
+  let is_frontend_tmp = function Var x -> not (Var.appears_in_source_code x) | _ -> false
+
   let rec is_pretty = function
     | Var _ ->
         true
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index b9685efb4..3f8074b63 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -689,6 +689,7 @@ module AliasTarget = struct
     | Size of Loc.t
     | Fgets of Loc.t
     | Nullity of Loc.t
+    | Top
   [@@deriving compare]
 
   let equal = [%compare.equal: t]
@@ -707,6 +708,8 @@ module AliasTarget = struct
         F.fprintf fmt "fgets(%a)" Loc.pp l
     | Nullity l ->
         F.fprintf fmt "nullity(%a)" Loc.pp l
+    | Top ->
+        F.fprintf fmt "T"
 
 
   let fgets l = Fgets l
@@ -715,10 +718,12 @@ module AliasTarget = struct
 
   let get_loc = function
     | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l | Nullity l ->
-        l
+        Some l
+    | Top ->
+        None
 
 
-  let use l x = Loc.equal l (get_loc x)
+  let use_loc l x = Option.value_map (get_loc x) ~default:false ~f:(Loc.equal l)
 
   let loc_map x ~f =
     match x with
@@ -734,18 +739,17 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Fgets l)
     | Nullity l ->
         Option.map (f l) ~f:(fun l -> Nullity l)
+    | Top ->
+        Some Top
 
 
   let ( <= ) ~lhs ~rhs = equal lhs rhs
 
-  let join x y =
-    assert (equal x y) ;
-    x
-
+  let join x y = if equal x y then x else Top
 
   let widen ~prev ~next ~num_iters:_ = join prev next
 
-  let is_unknown x = Loc.is_unknown (get_loc x)
+  let is_unknown x = Option.value_map (get_loc x) ~default:false ~f:Loc.is_unknown
 end
 
 (* Relations between values of logical variables(registers) and program variables
@@ -767,23 +771,76 @@ end
    AliasTarget.Empty relation, but is used when there is a program variable [i] for the length of
    the array. *)
 module AliasMap = struct
-  include AbstractDomain.Map (Ident) (AliasTarget)
+  module Key = struct
+    type t = IdentKey of Ident.t | JavaTmp of Loc.t [@@deriving compare]
+
+    let of_id id = IdentKey id
+
+    let of_java_tmp l = JavaTmp l
+
+    let pp f = function IdentKey id -> Ident.pp f id | JavaTmp l -> Loc.pp f l
+
+    let use_loc l = function JavaTmp l' -> Loc.equal l l' | IdentKey _ -> false
+  end
+
+  include AbstractDomain.InvertedMap (Key) (AliasTarget)
+
+  let some_non_top = function AliasTarget.Top -> None | v -> Some v
+
+  let add k v m = match some_non_top v with None -> remove k m | Some v -> add k v m
+
+  let join x y =
+    let join_v _key vx vy =
+      IOption.map2 vx vy ~f:(fun vx vy -> AliasTarget.join vx vy |> some_non_top)
+    in
+    merge join_v x y
+
+
+  let widen ~prev:x ~next:y ~num_iters =
+    let widen_v _key vx vy =
+      IOption.map2 vx vy ~f:(fun vx vy ->
+          AliasTarget.widen ~prev:vx ~next:vy ~num_iters |> some_non_top )
+    in
+    merge widen_v x y
+
 
   let pp : F.formatter -> t -> unit =
    fun fmt x ->
     if not (is_empty x) then
       let pp_sep fmt () = F.fprintf fmt ", @," in
-      let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Ident.pp k AliasTarget.pp v in
+      let pp1 fmt (k, v) = F.fprintf fmt "%a=%a" Key.pp k AliasTarget.pp v in
       F.pp_print_list ~pp_sep pp1 fmt (bindings x)
 
 
+  let find_id : Ident.t -> t -> AliasTarget.t option = fun id x -> find_opt (Key.of_id id) x
+
+  let find_java_tmp : Loc.t -> t -> AliasTarget.t option =
+   fun id x -> find_opt (Key.of_java_tmp id) x
+
+
   let load : Ident.t -> AliasTarget.t -> t -> t =
-   fun id a x -> if not (AliasTarget.is_unknown a) then add id a x else x
+   fun id tgt x ->
+    if AliasTarget.is_unknown tgt then x
+    else
+      let tgt =
+        match tgt with
+        | AliasTarget.Simple loc when Language.curr_language_is Java ->
+            Option.value (find_java_tmp loc x) ~default:tgt
+        | _ ->
+            tgt
+      in
+      add (Key.of_id id) tgt x
+
 
+  let forget : Loc.t -> t -> t =
+   fun l m -> filter (fun k y -> (not (Key.use_loc l k)) && not (AliasTarget.use_loc l y)) m
 
-  let forget : Loc.t -> t -> t = fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m
 
-  let find : Ident.t -> t -> AliasTarget.t option = find_opt
+  let store : Loc.t -> Ident.t -> t -> t =
+   fun l id x ->
+    if Language.curr_language_is Java && Loc.is_frontend_tmp l then
+      Option.value_map (find_id id x) ~default:x ~f:(fun tgt -> add (Key.of_java_tmp l) tgt x)
+    else x
 end
 
 module AliasRet = struct
@@ -823,7 +880,7 @@ module Alias = struct
 
   let bind_map : (AliasMap.t -> 'a) -> t -> 'a = fun f a -> f a.map
 
-  let find : Ident.t -> t -> AliasTarget.t option = fun x -> bind_map (AliasMap.find x)
+  let find_id : Ident.t -> t -> AliasTarget.t option = fun x -> bind_map (AliasMap.find_id x)
 
   let find_ret : t -> AliasTarget.t option = fun x -> AliasRet.get x.ret
 
@@ -833,9 +890,12 @@ module Alias = struct
    fun loc e a ->
     let a = lift_map (AliasMap.forget loc) a in
     match e with
-    | Exp.Var l when Loc.is_return loc ->
-        let update_ret retl = {a with ret= AliasRet.v retl} in
-        Option.value_map (find l a) ~default:a ~f:update_ret
+    | Exp.Var l ->
+        let a = lift_map (AliasMap.store loc l) a in
+        if Loc.is_return loc then
+          let update_ret retl = {a with ret= AliasRet.v retl} in
+          Option.value_map (find_id l a) ~default:a ~f:update_ret
+        else a
     | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i))
     | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) ->
         lift_map (AliasMap.load id (AliasTarget.SimplePlusA (loc, IntLit.neg i))) a
@@ -866,7 +926,8 @@ module Alias = struct
         a
 
 
-  let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp)
+  let remove_temp : Ident.t -> t -> t =
+   fun temp -> lift_map (AliasMap.remove (AliasMap.Key.of_id temp))
 end
 
 module CoreVal = struct
@@ -1350,22 +1411,27 @@ module MemReach = struct
     PowLoc.fold find_join locs Val.bot
 
 
-  let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find k m.alias
+  let find_alias : Ident.t -> _ t0 -> AliasTarget.t option = fun k m -> Alias.find_id k m.alias
 
   let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t option) option =
    fun k m ->
-    match Alias.find k m.alias with
+    match Alias.find_id k m.alias with
     | Some (AliasTarget.Simple l) ->
         Some (l, None)
     | Some (AliasTarget.SimplePlusA (l, i)) ->
         Some (l, Some i)
-    | Some (AliasTarget.Empty _ | AliasTarget.Size _ | AliasTarget.Fgets _ | AliasTarget.Nullity _)
+    | Some
+        ( AliasTarget.Empty _
+        | AliasTarget.Size _
+        | AliasTarget.Fgets _
+        | AliasTarget.Nullity _
+        | AliasTarget.Top )
     | None ->
         None
 
 
   let find_size_alias : Ident.t -> _ t0 -> Loc.t option =
-   fun k m -> match Alias.find k m.alias with Some (AliasTarget.Size l) -> Some l | _ -> None
+   fun k m -> match Alias.find_id k m.alias with Some (AliasTarget.Size l) -> Some l | _ -> None
 
 
   let find_ret_alias : _ t0 -> AliasTarget.t option = fun m -> Alias.find_ret m.alias
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 236a58b83..05731732c 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -892,7 +892,12 @@ module Collection = struct
   let size coll_exp =
     let exec _ ~ret:(ret_id, _) mem =
       let result = eval_collection_length coll_exp mem in
-      model_by_value result ret_id mem
+      let mem = model_by_value result ret_id mem in
+      match PowLoc.is_singleton_or_more (eval_collection_internal_array_locs coll_exp mem) with
+      | IContainer.Singleton loc ->
+          Dom.Mem.load_size_alias ret_id loc mem
+      | IContainer.Empty | IContainer.More ->
+          mem
     in
     {exec; check= no_check}
 
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index d6d830142..7691fac24 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -30,7 +30,9 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
   | Exp.Var x1, Exp.Var x2 -> (
     match (Mem.find_alias x1 m, Mem.find_alias x2 m) with
     | Some x1', Some x2' ->
-        AliasTarget.equal x1' x2' && not (Mem.is_rep_multi_loc (AliasTarget.get_loc x1') m)
+        AliasTarget.equal x1' x2'
+        && Option.value_map (AliasTarget.get_loc x1') ~default:false ~f:(fun l ->
+               not (Mem.is_rep_multi_loc l m) )
     | _, _ ->
         false )
   | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->
@@ -313,7 +315,8 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
         | AliasTarget.Size _
         | AliasTarget.Empty _
         | AliasTarget.Fgets _
-        | AliasTarget.Nullity _ )
+        | AliasTarget.Nullity _
+        | Top )
     | None ->
         Val.bot )
   | Exp.Lvar pvar ->
@@ -513,7 +516,7 @@ module Prune = struct
           let v = Mem.find lv mem in
           let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
-      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _) | None ->
+      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | Top) | None ->
           astate )
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
       match Mem.find_alias x mem with
@@ -530,7 +533,7 @@ module Prune = struct
           let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in
           let v' = Val.modify_itv itv_v v in
           update_mem_in_prune lv v' astate
-      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _) | None ->
+      | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _ | Top) | None ->
           astate )
     | _ ->
         astate
diff --git a/infer/src/istd/IOption.ml b/infer/src/istd/IOption.ml
index 478d01a86..51ba16943 100644
--- a/infer/src/istd/IOption.ml
+++ b/infer/src/istd/IOption.ml
@@ -14,3 +14,5 @@ let value_default_f ~f = function None -> f () | Some v -> v
 let if_none_evalopt ~f x = match x with None -> f () | Some _ -> x
 
 let if_none_eval = value_default_f
+
+let map2 x y ~f = match (x, y) with None, _ | _, None -> None | Some x, Some y -> f x y
diff --git a/infer/src/istd/IOption.mli b/infer/src/istd/IOption.mli
index 6b06d7037..16f2e273a 100644
--- a/infer/src/istd/IOption.mli
+++ b/infer/src/istd/IOption.mli
@@ -22,3 +22,6 @@ val if_none_eval : f:(unit -> 'a) -> 'a option -> 'a
 (** [if_none_eval ~f x] evaluates to [y] if [x=Some y] else to [f ()].
     Useful for terminating chains built with [if_none_evalopt]. 
     This is exactly the same as [value_default_f] but with a better name. *)
+
+val map2 : 'a option -> 'b option -> f:('a -> 'b -> 'c option) -> 'c option
+(** Like [Option.map2] but [f] may return [None]. *)
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
index 532d36b93..8f52d04f2 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/Array.java
@@ -68,4 +68,36 @@ class Array {
   void positive_alloc_Good() {
     a = new ArrayList<>(10);
   }
+
+  void iterate_collection_Good(ArrayList<Integer> a) {
+    if (a.size() > 10) {
+      int x = a.get(9);
+    }
+  }
+
+  void call_iterate_collection_Good() {
+    ArrayList<Integer> x = new ArrayList<Integer>();
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    this.iterate_collection_Good(x);
+  }
+
+  void iterate_collection_Bad(ArrayList<Integer> a) {
+    if (a.size() >= 5) {
+      int x = a.get(5);
+    }
+  }
+
+  void call_iterate_collection_Bad() {
+    ArrayList<Integer> x = new ArrayList<Integer>();
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    x.add(0);
+    this.iterate_collection_Bad(x);
+  }
 }
diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
index 1e35a1372..8300352a5 100644
--- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
@@ -1,3 +1,4 @@
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.call_iterate_collection_Bad():void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Through,Through,Through,Through,Through,Call,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5 by call to `void Array.iterate_collection_Bad(ArrayList)` ]
 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/Array.java, codetoanalyze.java.bufferoverrun.Array.negative_alloc_Bad():void, 1, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
 codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]