diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 14d20cf91..c9f5efe5f 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -526,6 +526,9 @@ module Name = struct
         |> QualifiedCppName.Set.of_list
       in
       function ObjcClass name -> not (QualifiedCppName.Set.mem name tagged_classes) | _ -> false
+
+
+    let objc_ns_enumerator = from_string "NSEnumerator"
   end
 
   module Set = PrettyPrintable.MakePPSet (struct
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 7de4f04cc..ac570aeac 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -271,6 +271,8 @@ module Name : sig
     val from_qual_name : QualifiedCppName.t -> t
 
     val protocol_from_qual_name : QualifiedCppName.t -> t
+
+    val objc_ns_enumerator : t
   end
 
   module Set : PrettyPrintable.PPSet with type elt = t
diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index 8360916a3..1c1dd3f07 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -546,6 +546,8 @@ module PowLoc = struct
         mk_known (LocSet.add l ploc)
 
 
+  let of_list locs = List.fold locs ~init:bot ~f:(fun acc loc -> add loc acc)
+
   let mem l = function
     | Bottom ->
         false
diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli
index cddde06dd..a750ddd3a 100644
--- a/infer/src/bufferoverrun/absLoc.mli
+++ b/infer/src/bufferoverrun/absLoc.mli
@@ -119,6 +119,8 @@ module PowLoc : sig
 
   val add : Loc.t -> t -> t
 
+  val of_list : Loc.t list -> t
+
   val exists : (Loc.t -> bool) -> t -> bool
 
   val mem : Loc.t -> t -> bool
diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml
index 873e5ed07..7875f052c 100644
--- a/infer/src/bufferoverrun/arrayBlk.ml
+++ b/infer/src/bufferoverrun/arrayBlk.ml
@@ -279,6 +279,14 @@ module ArrInfo = struct
         Itv.is_length_path_of prefix length
     | _ ->
         false
+
+
+  let prune_offset_le_size info =
+    match info with
+    | C {offset; size; stride} ->
+        C {offset= Itv.prune_le offset size; size; stride}
+    | Java _ | Top ->
+        info
 end
 
 include AbstractDomain.Map (Allocsite) (ArrInfo)
@@ -386,6 +394,8 @@ let prune_eq : t -> t -> t = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2
 
 let prune_ne : t -> t -> t = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2
 
+let prune_offset_le_size a = map ArrInfo.prune_offset_le_size a
+
 let set_length : Itv.t -> t -> t = fun length a -> map (ArrInfo.set_length length) a
 
 let set_stride : Z.t -> t -> t = fun stride a -> map (ArrInfo.set_stride stride) a
diff --git a/infer/src/bufferoverrun/arrayBlk.mli b/infer/src/bufferoverrun/arrayBlk.mli
index d938219c4..f98726744 100644
--- a/infer/src/bufferoverrun/arrayBlk.mli
+++ b/infer/src/bufferoverrun/arrayBlk.mli
@@ -58,6 +58,9 @@ val prune_eq : t -> t -> t
 val prune_ne : t -> t -> t
 (** [prune_ne x y] returns a pruned value of [x] by [!= y]. *)
 
+val prune_offset_le_size : t -> t
+(** Prune offset by [offset <= size] *)
+
 val minus_offset : t -> Itv.t -> t
 
 val plus_offset : t -> Itv.t -> t
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 8c9faa188..4be57ddfc 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -429,8 +429,6 @@ module Val = struct
 
   let prune_lt : t -> t -> t = prune_binop Binop.Lt
 
-  let prune_le : t -> t -> t = prune_binop Binop.Le
-
   let is_pointer_to_non_array x = (not (PowLoc.is_bot x.powloc)) && ArrayBlk.is_bot x.arrayblk
 
   (* In the pointer arithmetics, it returns top, if we cannot
@@ -565,6 +563,14 @@ module Val = struct
         itv_val ~non_int:false |> set_itv_updated_by_addition
     | Tptr ({desc= Tfun}, _) ->
         of_func_ptrs (FuncPtr.Set.of_path path)
+    | Tptr ({desc= Tstruct name}, _) when Typ.equal_name name Typ.Name.Objc.objc_ns_enumerator ->
+        (* NOTE: It generates a value of NSEnumerator specifically.  Especially, it assigns zero to
+           the offset, rather than a symbol, to avoid precision loss by limited handling of symbolic
+           values in the domain.  Although this is an unsound design choice, we expect it should not
+           that harmful for calculating WCET. *)
+        let allocsite = SPath.deref ~deref_kind:Deref_CPointer path |> Allocsite.make_symbol in
+        let size = Itv.of_length_path ~is_void:false path in
+        {bot with arrayblk= ArrayBlk.make_c allocsite ~offset:Itv.zero ~size ~stride:Itv.one}
     | Tptr (elt, _) ->
         if is_java || SPath.is_this path then
           let deref_kind =
@@ -1365,20 +1371,13 @@ module AliasMap = struct
 
 
   let add_iterator_next_object_alias ~ret_id ~iterator x =
-    let accum_next_object_alias rhs tgt acc =
-      match tgt with
-      | AliasTarget.IteratorSimple _ ->
-          add_alias ~lhs:(KeyLhs.of_id ret_id) ~rhs
-            (AliasTarget.IteratorNextObject {objc_tmp= None})
-            acc
-      | _ ->
-          acc
-    in
     let open IOption.Let_syntax in
     M.find_opt (KeyLhs.of_id iterator) x
     >>= AliasTargets.find_simple_alias
-    >>= (fun rhs -> M.find_opt (KeyLhs.of_loc rhs) x)
-    >>| (fun tgts -> AliasTargets.fold accum_next_object_alias tgts x)
+    >>| (fun rhs ->
+          add_alias ~lhs:(KeyLhs.of_id ret_id) ~rhs
+            (AliasTarget.IteratorNextObject {objc_tmp= None})
+            x )
     |> Option.value ~default:x
 end
 
@@ -2083,11 +2082,6 @@ module MemReach = struct
 
   let add_iterator_alias id m = add_iterator_offset_alias id m |> add_iterator_simple_alias id
 
-  let add_iterator_alias_objc id m =
-    let array_loc = find_stack (Loc.of_id id) m |> Val.get_pow_loc in
-    {m with alias= Alias.add_iterator_simple_alias id array_loc m.alias}
-
-
   let incr_iterator_offset_alias id m = {m with alias= Alias.incr_iterator_offset_alias id m.alias}
 
   let add_iterator_has_next_alias ~ret_id ~iterator m =
@@ -2464,10 +2458,6 @@ module Mem = struct
 
   let add_iterator_alias : Ident.t -> t -> t = fun id -> map ~f:(MemReach.add_iterator_alias id)
 
-  let add_iterator_alias_objc : Ident.t -> t -> t =
-   fun id -> map ~f:(MemReach.add_iterator_alias_objc id)
-
-
   let incr_iterator_offset_alias : Exp.t -> t -> t =
    fun iterator m ->
     match iterator with Exp.Var id -> map ~f:(MemReach.incr_iterator_offset_alias id) m | _ -> m
@@ -2482,13 +2472,8 @@ module Mem = struct
         m
 
 
-  let add_iterator_next_object_alias : Ident.t -> Exp.t -> t -> t =
-   fun ret_id iterator m ->
-    match iterator with
-    | Exp.Var iterator ->
-        map ~f:(MemReach.add_iterator_next_object_alias ~ret_id ~iterator) m
-    | _ ->
-        m
+  let add_iterator_next_object_alias : ret_id:Ident.t -> iterator:Ident.t -> t -> t =
+   fun ~ret_id ~iterator m -> map ~f:(MemReach.add_iterator_next_object_alias ~ret_id ~iterator) m
 
 
   let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli
index 346271851..8fcd8899e 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.mli
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli
@@ -227,10 +227,6 @@ module Val : sig
   (** Pruning semantics for [Binop.Lt]. This prunes value of [x] when given [x < y], i.e.,
       [prune_lt x y]. *)
 
-  val prune_le : t -> t -> t
-  (** Pruning semantics for [Binop.Lt]. This prunes value of [x] when given [x <= y], i.e.,
-      [prune_le x y]. *)
-
   val prune_ne_zero : t -> t
   (** Prune value of [x] when given [x != 0] *)
 
@@ -592,7 +588,7 @@ module Mem : sig
   val add_iterator_has_next_alias : Ident.t -> Exp.t -> t -> t
   (** Add an [AliasTarget.IteratorHasNext] alias when [ident = iterator.hasNext()] is called *)
 
-  val add_iterator_next_object_alias : Ident.t -> Exp.t -> t -> t
+  val add_iterator_next_object_alias : ret_id:Ident.t -> iterator:Ident.t -> t -> t
   (** Add an [AliasTarget.IteratorNextObject] alias when [ident = iterator.nextObject()] is called *)
 
   val incr_iterator_simple_alias_on_call : eval_sym_trace -> callee_exit_mem:no_oenv_t -> t -> t
@@ -602,8 +598,6 @@ module Mem : sig
   (** Add [AliasTarget.IteratorSimple] and [AliasTarget.IteratorOffset] aliases when
       [Iteratable.iterator()] is called *)
 
-  val add_iterator_alias_objc : Ident.t -> t -> t
-
   val incr_iterator_offset_alias : Exp.t -> t -> t
   (** Update iterator offset alias when [iterator.next()] is called *)
 
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index e25b69099..2402ffd0d 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -1142,34 +1142,34 @@ module NSCollection = struct
 
 
   let iterator coll_exp =
-    let exec {integer_type_widths; location} ~ret:(ret_id, _) mem =
-      let traces = Trace.(Set.singleton location ArrayDeclaration) in
-      let array_v = Sem.eval integer_type_widths coll_exp mem in
-      let array_loc = Dom.Val.get_all_locs array_v in
-      let offset_loc = PowLoc.append_field ~fn:BufferOverrunField.objc_iterator_offset array_loc in
-      let mem = Dom.Mem.add_heap_set offset_loc Dom.Val.Itv.zero mem in
-      model_by_value (Dom.Val.of_pow_loc ~traces array_loc) ret_id mem
-      |> Dom.Mem.add_heap_set array_loc array_v
-      |> Dom.Mem.add_iterator_alias_objc ret_id
+    let exec {integer_type_widths= _; location} ~ret:(id, _) mem =
+      let elements_locs = eval_collection_internal_array_locs coll_exp mem in
+      let v = Dom.Mem.find_set elements_locs mem |> Dom.Val.set_array_offset location Itv.zero in
+      model_by_value v id mem
     in
     {exec; check= no_check}
 
 
   let next_object iterator =
-    let exec {integer_type_widths} ~ret:(id, _) mem =
-      let iterator_v = Sem.eval integer_type_widths iterator mem in
-      let traces = Dom.Val.get_traces iterator_v in
-      let offset_loc =
-        Dom.Val.get_pow_loc iterator_v
-        |> PowLoc.append_field ~fn:BufferOverrunField.objc_iterator_offset
+    let exec _ ~ret:(ret_id, _) mem =
+      let iterator_locs =
+        Dom.Mem.find_simple_alias iterator mem
+        |> List.filter_map ~f:(fun (l, i) -> if IntLit.iszero i then Some l else None)
+        |> PowLoc.of_list
       in
-      let next_offset_v =
-        Dom.Mem.find_set offset_loc mem |> Dom.Val.get_itv |> Itv.incr |> Dom.Val.of_itv
+      let iterator_v = Dom.Mem.find_set iterator_locs mem in
+      let arrayblk = ArrayBlk.plus_offset (Dom.Val.get_array_blk iterator_v) Itv.one in
+      let iterator_v' = {iterator_v with arrayblk} in
+      let return_v =
+        (* NOTE: It joins zero to avoid unreachable nodes due to the following hack.  The
+           [nextObject] returns the offset of the enumerator instead of an object elements,
+           which helps the cost checker select the offset as a control variable, for example,
+           [while(obj = [enumerator nextObject]) { ... }]. *)
+        ArrayBlk.get_offset arrayblk |> Itv.join Itv.zero |> Dom.Val.of_itv
       in
-      let locs = eval_collection_internal_array_locs iterator mem in
-      model_by_value (Dom.Val.of_pow_loc ~traces locs) id mem
-      |> Dom.Mem.add_heap_set offset_loc next_offset_v
-      |> Dom.Mem.add_iterator_next_object_alias id iterator
+      model_by_value return_v ret_id mem
+      |> Dom.Mem.add_heap_set iterator_locs iterator_v'
+      |> Dom.Mem.add_iterator_next_object_alias ~ret_id ~iterator
     in
     {exec; check= no_check}
 end
@@ -1712,7 +1712,7 @@ module Call = struct
         &:: "arrayByAddingObjectsFromArray:" <>$ capt_exp $+ capt_exp
         $--> NSCollection.new_collection_by_add_all
       ; +PatternMatch.ObjectiveC.implements "NSEnumerator"
-        &:: "nextObject" <>$ capt_exp $--> NSCollection.next_object
+        &:: "nextObject" <>$ capt_var_exn $--> NSCollection.next_object
       ; +PatternMatch.ObjectiveC.implements "NSFileManager"
         &:: "contentsOfDirectoryAtURL:includingPropertiesForKeys:options:error:"
         &--> NSCollection.new_collection
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index f4045af32..739e4643d 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -590,27 +590,18 @@ module Prune = struct
             update_mem_in_prune lv_linked_list_index pruned_v acc ) )
 
 
-  let nscollection_length_of_iterator loc mem =
-    let arr_locs =
-      Mem.find loc mem |> Val.get_all_locs
-      |> PowLoc.append_field ~fn:BufferOverrunField.objc_collection_internal_array
-    in
-    eval_array_locs_length arr_locs mem
-
-
   let prune_iterator_offset_objc next_object mem acc =
     let tgts = Mem.find_alias_loc next_object mem in
     AliasTargets.fold
-      (fun rhs tgt acc ->
+      (fun iterator tgt acc ->
         match tgt with
         | AliasTarget.IteratorNextObject _ ->
-            let array_length = nscollection_length_of_iterator rhs mem in
-            let iterator_offset_loc =
-              Loc.append_field rhs BufferOverrunField.objc_iterator_offset
+            let iterator_v = Mem.find iterator mem in
+            let iterator_v' =
+              { iterator_v with
+                arrayblk= Val.get_array_blk iterator_v |> ArrayBlk.prune_offset_le_size }
             in
-            let iterator_offset_v = Mem.find iterator_offset_loc mem in
-            let iterator_offset_v' = Val.prune_le iterator_offset_v array_length in
-            update_mem_in_prune iterator_offset_loc iterator_offset_v' acc
+            update_mem_in_prune iterator iterator_v' acc
         | _ ->
             acc )
       tgts acc
diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/arc_enumerator.m b/infer/tests/codetoanalyze/objc/autoreleasepool/arc_enumerator.m
index bc3441725..1f61705fc 100644
--- a/infer/tests/codetoanalyze/objc/autoreleasepool/arc_enumerator.m
+++ b/infer/tests/codetoanalyze/objc/autoreleasepool/arc_enumerator.m
@@ -49,11 +49,17 @@ typedef BOOL (^Filter)(id);
                                       }];
 }
 
-- (void)callMyEnumerator_linear_FN:(NSArray*)x {
+// The cost analyzer cannot reason the amortized complexity.
+- (void)callMyEnumerator_linear_FP:(NSArray*)x {
   MyEnumerator* enumerator = [self makeMyEnumerator_zero:x];
   id s;
   while (s = [enumerator nextObject]) {
   }
 }
 
+- (void)callMyEnumerator_nextObject_linear:(NSArray*)x {
+  MyEnumerator* enumerator = [self makeMyEnumerator_zero:x];
+  id s = [enumerator nextObject];
+}
+
 @end
diff --git a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
index 70c525cfd..51b07e915 100644
--- a/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
+++ b/infer/tests/codetoanalyze/objc/autoreleasepool/cost-issues.exp
@@ -24,12 +24,13 @@ codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callGiveMeObject_line
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callMutableCopyObject_zero:x:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.callNewObject_zero:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_caller.m, ArcCaller.dealloc, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.callMyEnumerator_linear_FN:, 1,  OnUIThread:false, []
+codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.callMyEnumerator_linear_FP:, (x->elements.length.ub + 1) × (x->elements.length.ub + 2),  OnUIThread:false, [{x->elements.length.ub + 2},Loop,{x->elements.length.ub + 1},Call to MyEnumerator.nextObject,Loop]
+codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.callMyEnumerator_nextObject_linear:, (x->elements.length.ub + 1),  OnUIThread:false, [{x->elements.length.ub + 1},Call to MyEnumerator.nextObject,Loop]
 codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.dealloc, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_enumerator.m, ArcEnumerator.makeMyEnumerator_zero:, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_enumerator.m, MyEnumerator.dealloc, 0,  OnUIThread:false, []
 codetoanalyze/objc/autoreleasepool/arc_enumerator.m, MyEnumerator.initWithArray:filter:, 0,  OnUIThread:false, []
-codetoanalyze/objc/autoreleasepool/arc_enumerator.m, MyEnumerator.nextObject, |self->_filter|,  OnUIThread:false, []
+codetoanalyze/objc/autoreleasepool/arc_enumerator.m, MyEnumerator.nextObject, (self->_enumerator.length + 1) × |self->_filter|,  OnUIThread:false, [{self->_enumerator.length + 1},Loop]
 codetoanalyze/objc/autoreleasepool/arc_enumerator.m, objc_blockArcEnumerator.makeMyEnumerator_zero:_1, 1,  OnUIThread:false, [autorelease,Call to NoArcCallee.giveMeObject,Modeled call to NSObject.autorelease]
 codetoanalyze/objc/autoreleasepool/arc_keyed_unarchiver.m, ArcKeyedUnarchiver.callInitForReadingFromData_constant:data:, 1,  OnUIThread:false, [autorelease,Modeled call to NSKeyedUnarchiver.initForReadingFromData:error:]
 codetoanalyze/objc/autoreleasepool/arc_keyed_unarchiver.m, ArcKeyedUnarchiver.callInitForReadingWithData_constant:data:, 1,  OnUIThread:false, [autorelease,Modeled call to NSKeyedUnarchiver.initForReadingWithData:]
diff --git a/infer/tests/codetoanalyze/objc/performance/NSArray.m b/infer/tests/codetoanalyze/objc/performance/NSArray.m
index 77647a0dd..34d93ff89 100644
--- a/infer/tests/codetoanalyze/objc/performance/NSArray.m
+++ b/infer/tests/codetoanalyze/objc/performance/NSArray.m
@@ -51,7 +51,7 @@ NSArray* nsarray_init_with_objects_constant() {
   }
 }
 
-NSArray* nsarray_array_with_objects_constant() {
+NSArray* nsarray_array_with_objects_constant_FP() {
   NSDate* aDate = [NSDate distantFuture];
   NSValue* aValue = @(5);
   NSString* aString = @"hello";
@@ -166,13 +166,13 @@ void nsarray_enumerator_linear(NSArray* array) {
   }
 }
 
-void nsarray_enumerator_param_linear_FN(NSEnumerator* enumerator) {
+void nsarray_enumerator_param_linear(NSEnumerator* enumerator) {
   id obj;
   while (obj = [enumerator nextObject]) {
   }
 }
 
-void call_nsarray_enumerator_param_linear_FN(NSArray* array) {
+void call_nsarray_enumerator_param_linear(NSArray* array) {
   NSEnumerator* enumerator = [array objectEnumerator];
   nsarray_enumerator_param_linear_FN(enumerator);
 }
diff --git a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp
index f01847a57..25d90c747 100644
--- a/infer/tests/codetoanalyze/objc/performance/cost-issues.exp
+++ b/infer/tests/codetoanalyze/objc/performance/cost-issues.exp
@@ -1,17 +1,17 @@
 ${XCODE_ISYSROOT}/System/Library/Frameworks/Foundation.framework/Headers/NSArray.h, NSArray.indexOfObject:inSortedRange:options:usingComparator:[objc_blocknsarray_binary_search_log_FN_1], 0,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, call_nsarray_enumerator_param_linear_FN, 12,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, call_nsarray_enumerator_param_linear, 6,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_access_constant, 50,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_access_linear, 3 + 7 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_add_object_constant, 8,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_add_objects_from_array_linear, 9 + 3 ⋅ append_array->elements.length.ub + append_array->elements.length.ub + 3 ⋅ (append_array->elements.length.ub + 1),  OnUIThread:false, [{append_array->elements.length.ub + 1},Loop,{append_array->elements.length.ub},Modeled call to NSArray.arrayByAddingObjectsFromArray:,{append_array->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_array_with_objects_constant, 27,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_array_with_objects_constant_FP, ⊤,  OnUIThread:false, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_binary_search_log_FN, 10,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_contains_object_linear, 3 + array->elements.length.ub,  OnUIThread:false, [{array->elements.length.ub},Modeled call to NSArray.containsObject:]
 codetoanalyze/objc/performance/NSArray.m, nsarray_copy_linear, 6 + 3 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_count_bounded_linear, 3 + 3 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_empty_array_constant, 8,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear, 6 + 4 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_param_linear_FN, 7,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear, 6 + 8 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_param_linear, 2 + 5 ⋅ (enumerator.length + 1),  OnUIThread:false, [{enumerator.length + 1},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_find_linear, 4 + 9 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_first_object_constant, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_get_first_constant, 27,  OnUIThread:false, []
@@ -21,10 +21,10 @@ codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_copy_linear, 7
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_array_linear, 6 + 3 ⋅ array->elements.length.ub + array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Modeled call to NSArray.initWithArray:,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_with_objects_constant, 39,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_is_equal_to_array_linear, 4 + array1->elements.length.ub,  OnUIThread:false, [{array1->elements.length.ub},Modeled call to NSArray.isEqualToArray:]
-codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear, 6 + 4 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear, 6 + 8 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_last_object_constant, 4,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_constant, 25,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_linear, 5 + array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_constant, 26,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSArray.m, nsarray_next_object_linear, 5 + 5 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_object_at_indexed_constant, 34,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_sort_using_descriptors_constant, 39,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSArray.m, nsarray_sort_using_descriptors_nlogn, 9 + array->elements.length.ub × log(array->elements.length.ub),  OnUIThread:false, [{array->elements.length.ub},Modeled call to NSArray.sortedArrayUsingDescriptors:,{array->elements.length.ub},Modeled call to NSArray.sortedArrayUsingDescriptors:]
@@ -36,9 +36,9 @@ codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_alloc_with_zone_init
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_dictionary_constant, 13,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_dictionary_with_objects_linear, 14 + 15 ⋅ n_entries + 3 ⋅ n_entries + 2 ⋅ (1+max(0, n_entries)) + 4 ⋅ (1+max(0, n_entries)),  OnUIThread:false, [{1+max(0, n_entries)},Loop,{1+max(0, n_entries)},Loop,{n_entries},Loop,{n_entries},Loop]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_call_constant, 65,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_constant, 69,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerator_linear, 5 + dict->elements.length.ub + 4 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop,{dict->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_fast_enumerate_linear, 5 + dict->elements.length.ub + 4 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop,{dict->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_constant, 74,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerator_linear, 5 + 5 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop]
+codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_fast_enumerate_linear, 5 + 5 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_find_key_constant, 19,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_init_dictionary_constant, 3,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_init_literal_constant, 45,  OnUIThread:false, []
@@ -60,19 +60,19 @@ codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_constant, 17,
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_in_loop_constant, 182,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_in_loop_constant, 51,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_linear, 3 + 11 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSMutableDictionary.m, nsmutabledictionary_set_element_in_loop_linear, 5 + 5 ⋅ dict->elements.length.ub + 4 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop,{dict->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSMutableDictionary.m, nsmutabledictionary_set_element_in_loop_linear, 5 + 9 ⋅ (dict->elements.length.ub + 1),  OnUIThread:false, [{dict->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSMutableString.m, copy_string_constant_FP, 11 + 3 ⋅ str3.length.ub + str3.length.ub + 3 ⋅ (str3.length.ub + 1),  OnUIThread:false, [{str3.length.ub + 1},Loop,{str3.length.ub},Modeled call to NSMutableString.appendString:,{str3.length.ub},Loop]
 codetoanalyze/objc/performance/NSMutableString.m, nsmstring_append_string_constant, 14 + 3 ⋅ (str.length.ub + 5) + 3 ⋅ (str.length.ub + 6),  OnUIThread:false, [{str.length.ub + 6},Loop,{str.length.ub + 5},Loop]
 codetoanalyze/objc/performance/NSMutableString.m, nsmstring_append_string_linear, 5 + str2.length.ub + 3 ⋅ (str2.length.ub + str1.length.ub) + 3 ⋅ (str2.length.ub + str1.length.ub + 1),  OnUIThread:false, [{str2.length.ub + str1.length.ub + 1},Loop,{str2.length.ub + str1.length.ub},Loop,{str2.length.ub},Modeled call to NSMutableString.appendString:]
-codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_empty_constant, 13,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_iterate_linear, 5 + ordered_set->elements.length.ub + 4 ⋅ (ordered_set->elements.length.ub + 1),  OnUIThread:false, [{ordered_set->elements.length.ub + 1},Loop,{ordered_set->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_with_array_linear, 10 + array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Call to nsordered_set_iterate_linear,Loop,{array->elements.length.ub},Call to nsordered_set_iterate_linear,Loop]
-codetoanalyze/objc/performance/NSSet.m, nsset_enumerator_linear, 6 + 4 ⋅ set->elements.length.ub + 4 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop,{set->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_empty_constant, 14,  OnUIThread:false, []
+codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_iterate_linear, 5 + 5 ⋅ (ordered_set->elements.length.ub + 1),  OnUIThread:false, [{ordered_set->elements.length.ub + 1},Loop]
+codetoanalyze/objc/performance/NSOrderedSet.m, nsordered_set_with_array_linear, 10 + 5 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Call to nsordered_set_iterate_linear,Loop]
+codetoanalyze/objc/performance/NSSet.m, nsset_enumerator_linear, 6 + 8 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSSet.m, nsset_init_constant, 9,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSSet.m, nsset_init_with_array_linear, 7 + 3 ⋅ array->elements.length.ub + 3 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
 codetoanalyze/objc/performance/NSSet.m, nsset_init_with_set_constant, 6,  OnUIThread:false, []
-codetoanalyze/objc/performance/NSSet.m, nsset_iterate_linear, 6 + 4 ⋅ set->elements.length.ub + 4 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop,{set->elements.length.ub},Loop]
-codetoanalyze/objc/performance/NSSet.m, nsset_next_object_linear, 5 + set->elements.length.ub + 4 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop,{set->elements.length.ub},Loop]
+codetoanalyze/objc/performance/NSSet.m, nsset_iterate_linear, 6 + 8 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop]
+codetoanalyze/objc/performance/NSSet.m, nsset_next_object_linear, 5 + 5 ⋅ (set->elements.length.ub + 1),  OnUIThread:false, [{set->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/NSString.m, call_component_separated_by_char_constant, 46,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSString.m, call_init_with_string_constant, 15,  OnUIThread:false, []
 codetoanalyze/objc/performance/NSString.m, component_seperated_by_char_linear, 6 + m.length.ub + 3 ⋅ (-1+max(2, m.length.ub)) + 3 ⋅ (max(2, m.length.ub)),  OnUIThread:false, [{max(2, m.length.ub)},Loop,{-1+max(2, m.length.ub)},Loop,{m.length.ub},Modeled call to NSString.componentsSeparatedByString:]
@@ -100,12 +100,12 @@ codetoanalyze/objc/performance/araii.m, Araii.dealloc, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, Araii.initWithBuffer, 15,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, Araii.setBuffer:, 4,  OnUIThread:false, []
 codetoanalyze/objc/performance/araii.m, memory_leak_raii_main, 18,  OnUIThread:false, []
-codetoanalyze/objc/performance/block.m, block_multiply_array_linear, 13 + 5 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Call to objc_blockblock_multiply_array_linear_1,Loop,{array->elements.length.ub},Call to objc_blockblock_multiply_array_linear_1,Loop]
+codetoanalyze/objc/performance/block.m, block_multiply_array_linear, 13 + 9 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Call to objc_blockblock_multiply_array_linear_1,Loop]
 codetoanalyze/objc/performance/block.m, call_wrapper_runBlockA_linear, 11 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to loop_linear,Loop,{a},Call to loop_linear,Loop]
 codetoanalyze/objc/performance/block.m, doBlockA_direct_block_linear, 10 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to runBlockA[objc_blockdoBlockA_direct_block_linear_3],Call to objc_blockdoBlockA_direct_block_linear_3,Call to loop_linear,Loop,{a},Call to runBlockA[objc_blockdoBlockA_direct_block_linear_3],Call to objc_blockdoBlockA_direct_block_linear_3,Call to loop_linear,Loop]
 codetoanalyze/objc/performance/block.m, doBlockA_linear, 12 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to runBlockA[objc_blockdoBlockA_linear_2],Call to objc_blockdoBlockA_linear_2,Call to loop_linear,Loop,{a},Call to runBlockA[objc_blockdoBlockA_linear_2],Call to objc_blockdoBlockA_linear_2,Call to loop_linear,Loop]
 codetoanalyze/objc/performance/block.m, loop_linear, 3 + 3 ⋅ x + 2 ⋅ (1+max(0, x)),  OnUIThread:false, [{1+max(0, x)},Loop,{x},Loop]
-codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_1, 8 + 5 ⋅ array->elements.length.ub + 4 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop,{array->elements.length.ub},Loop]
+codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_1, 8 + 9 ⋅ (array->elements.length.ub + 1),  OnUIThread:false, [{array->elements.length.ub + 1},Loop]
 codetoanalyze/objc/performance/block.m, objc_blockcall_wrapper_runBlockA_linear_4, 5 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to loop_linear,Loop,{a},Call to loop_linear,Loop]
 codetoanalyze/objc/performance/block.m, objc_blockdoBlockA_direct_block_linear_3, 5 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to loop_linear,Loop,{a},Call to loop_linear,Loop]
 codetoanalyze/objc/performance/block.m, objc_blockdoBlockA_linear_2, 5 + 3 ⋅ a + 2 ⋅ (1+max(0, a)),  OnUIThread:false, [{1+max(0, a)},Call to loop_linear,Loop,{a},Call to loop_linear,Loop]
diff --git a/infer/tests/codetoanalyze/objc/performance/issues.exp b/infer/tests/codetoanalyze/objc/performance/issues.exp
index bb7fa4dd9..3b5867a0d 100644
--- a/infer/tests/codetoanalyze/objc/performance/issues.exp
+++ b/infer/tests/codetoanalyze/objc/performance/issues.exp
@@ -1,14 +1,21 @@
+codetoanalyze/objc/performance/NSArray.m, nsarray_array_with_objects_constant_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSArray.m, nsarray_empty_array_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/objc/performance/NSArray.m, nsarray_enumerator_linear, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [1, array->elements.length.ub + 1]):signed64]
 codetoanalyze/objc/performance/NSArray.m, nsarray_init_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/objc/performance/NSArray.m, nsarray_iterate_linear, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [1, array->elements.length.ub + 1]):signed64]
+codetoanalyze/objc/performance/NSDictionary.m, nsdictionary_enumerate_constant, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [1, 3] Size: 2]
 codetoanalyze/objc/performance/NSFileManager.m, contents_of_directory_at_url_constant, 7, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSMutableArray.m, nsarray_new_constant, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_constant, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Through,Through,Through,Array access: Offset: 0 Size: 0]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_remove_in_loop_constant, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Set array size,<Length trace>,Assignment,Set array size,Array access: Offset: [0, 9] Size: [1, 10]]
 codetoanalyze/objc/performance/NSMutableArray.m, nsmarray_set_linear, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSNumber.intValue,Binary operation: ([-oo, +oo] + 1):signed32]
+codetoanalyze/objc/performance/NSSet.m, nsset_enumerator_linear, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [1, set->elements.length.ub + 1]):signed64]
 codetoanalyze/objc/performance/NSSet.m, nsset_init_constant, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/objc/performance/NSSet.m, nsset_iterate_linear, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [1, set->elements.length.ub + 1]):signed64]
 codetoanalyze/objc/performance/NSString.m, init_string_constant, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop]
 codetoanalyze/objc/performance/NSString.m, replace_linear_FP, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: NSString.stringByReplacingOccurrencesOfString:withString:,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/objc/performance/block.m, objc_blockblock_multiply_array_linear_1, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([0, +oo] + [1, array->elements.length.ub + 1]):signed64]
 codetoanalyze/objc/performance/compound_loop_guard.m, compound_while, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/compound_loop_guard.m, nested_while_and_or_constant, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/objc/performance/compound_loop_guard.m, nested_while_and_or_constant, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]