diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 2774ed4cd..5e941fb82 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -412,7 +412,9 @@ module StdArray = struct
     (* TODO? use size *)
     let exec {integer_type_widths} ~ret:(id, _) mem =
       L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ;
-      BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem
+      Dom.Mem.add_stack (Loc.of_id id)
+        (Sem.eval_lindex integer_type_widths array_exp index_exp mem)
+        mem
     and check {location; integer_type_widths} mem cond_set =
       BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem
         location cond_set
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml
index 865ed36f7..e55786704 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.ml
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml
@@ -44,8 +44,6 @@ module Exec = struct
     else mem
 
 
-  let load_val id v mem = load_locs id (Dom.Val.get_all_locs v) mem
-
   let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values
       ~dimension mem =
     match typ.Typ.desc with
diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli
index 715f706b3..7d83cccc0 100644
--- a/infer/src/bufferoverrun/bufferOverrunUtils.mli
+++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli
@@ -26,8 +26,6 @@ end
 module Exec : sig
   val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
-  val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
-
   val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int
 
   val init_c_array_fields :
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index cbec7b353..595136ca6 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -84,6 +84,7 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
 codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
+codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_contents_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, call_length4_2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Array declaration,Array access: Offset: 11 Size: 10 by call to `length4` ]
 codetoanalyze/cpp/bufferoverrun/std_string.cpp, compare_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp
index aba4ad3ba..14b045643 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/std_array.cpp
@@ -46,7 +46,7 @@ void std_array_contents_Good() {
   a[a[0]] = 0;
 }
 
-void std_array_contents_Bad_FN() {
+void std_array_contents_Bad() {
   std::array<int, 10> a;
   a[0] = 10;
   a[a[0]] = 0;