diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index c91209d99f2..52090502a23 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/infer/src/bufferoverrun/bounds.ml
@@ -950,12 +950,12 @@ module Bound = struct
   let plus_l : weak:bool -> t -> t -> t =
     plus_exact ~otherwise:(fun x y ->
         match (x, y) with
-        | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
-        | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
-            Linear (Z.(c1 + d1 + c2), x2)
-        | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
-        | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) ->
-            Linear (Z.(c1 - d1 + c2), x2)
+        | MinMax (c1, Plus, Max, d1, x1), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Plus, Max, d1, x1) ->
+            mk_MinMaxB (Max, (Linear (Z.(c1 + d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_one x1) x2)))
+        | MinMax (c1, Minus, Min, d1, x1), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Minus, Min, d1, x1) ->
+            mk_MinMaxB (Max, (Linear (Z.(c1 - d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_minus_one x1) x2)))
         | _, _ ->
             MInf )
 
@@ -963,12 +963,12 @@ module Bound = struct
   let plus_u : weak:bool -> t -> t -> t =
     plus_exact ~otherwise:(fun x y ->
         match (x, y) with
-        | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
-        | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) ->
-            Linear (Z.(c1 + d1 + c2), x2)
-        | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2)
-        | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) ->
-            Linear (Z.(c1 - d1 + c2), x2)
+        | MinMax (c1, Plus, Min, d1, x1), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Plus, Min, d1, x1) ->
+            mk_MinMaxB (Min, (Linear (Z.(c1 + d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_one x1) x2)))
+        | MinMax (c1, Minus, Max, d1, x1), Linear (c2, x2)
+        | Linear (c2, x2), MinMax (c1, Minus, Max, d1, x1) ->
+            mk_MinMaxB (Min, (Linear (Z.(c1 - d1 + c2), x2)), (Linear (Z.(c1 + c2), SymLinear.plus (SymLinear.singleton_minus_one x1) x2)))
         | _, _ ->
             PInf )
 
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index e37fb638e31..165653092e0 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -347,6 +347,10 @@ module ArrayAccessCondition = struct
       Bound.is_not_infty (ItvPure.ub real_idx) && Bound.le (ItvPure.ub size) (ItvPure.ub real_idx)
     then {report_issue_type= Issue IssueType.buffer_overrun_l2; propagate= false}
       (* symbolic il >= sl, probably an error *)
+    else if
+      Bound.is_infty (ItvPure.ub real_idx) && Bound.is_not_infty (ItvPure.ub size) 
+    then {report_issue_type= Issue IssueType.buffer_overrun_l3; propagate= false}
+      (* su < iu = +oo, probably an error *)
     else if
       Bound.is_symbolic (ItvPure.lb real_idx) && Bound.le (ItvPure.lb size) (ItvPure.lb real_idx)
     then {report_issue_type= Issue IssueType.buffer_overrun_s2; propagate= true}
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index fbee9e3b930..484a13314d4 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -16,6 +16,7 @@ module Sem = BufferOverrunSemantics
 module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 module TypModels = BufferOverrunTypModels
+module BoField = BufferOverrunField
 
 module ModelEnv = struct
   type model_env =
@@ -52,7 +53,23 @@ module Exec = struct
         mem
 
 
-  let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values
+  let rec decl_local_struct_fields_loc: ModelEnv.model_env -> Loc.t -> Struct.fields -> Dom.Mem.t * int -> Dom.Mem.t * int =
+    fun model_env loc fields (mem, inst_num) ->
+      match fields with
+      | field :: tl -> (
+        match field with
+        | (fn, typ, _) -> (
+          match typ.desc with
+          | Tarray {elt= _; length; stride} ->
+            let child_loc = BoField.Field {prefix= loc; fn; typ = (Some typ)} in
+            let stride = Option.map ~f:IntLit.to_int_exn stride in
+            let (mem, inst_num) = decl_local_array model_env child_loc typ ~length ?stride ~inst_num
+              ~represents_multiple_values:false ~dimension:1 mem
+            in
+              decl_local_struct_fields_loc model_env loc tl (mem, inst_num)
+          | _ -> decl_local_struct_fields_loc model_env loc tl (mem, inst_num)))
+      | [] -> (mem, inst_num)
+  and decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values
       ~dimension mem =
     match typ.Typ.desc with
     | Typ.Tarray {elt= typ; length; stride} ->
@@ -60,6 +77,13 @@ module Exec = struct
         decl_local_array model_env loc typ ~length ?stride ~inst_num ~represents_multiple_values
           ~dimension mem
     | Typ.Tstruct typname -> (
+      let mem = (
+        match Tenv.lookup tenv typname with
+        | Some {fields} -> 
+            let (mem, _) = decl_local_struct_fields_loc model_env loc fields (mem, 1) in mem
+        | None -> mem 
+      ) 
+      in 
       match TypModels.dispatch tenv typname with
       | Some (CArray {element_typ; length}) ->
           decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num