diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 22f5bd2b0..d69da13ef 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -567,6 +567,13 @@ module StdArray = struct
     {exec; check= no_check}
 end
 
+let array_empty_exec ret_id array_v mem =
+  let traces = Dom.Val.get_traces array_v in
+  let size = ArrayBlk.sizeof (Dom.Val.get_array_blk array_v) in
+  let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
+  model_by_value empty ret_id mem
+
+
 module StdBasicString = struct
   (* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)
   let constructor_from_char_ptr tgt src len =
@@ -616,11 +623,8 @@ module StdBasicString = struct
 
   let empty e =
     let exec {integer_type_widths} ~ret:(ret_id, _) mem =
-      let v = Sem.eval integer_type_widths e mem in
-      let traces = Dom.Val.get_traces v in
-      let size = ArrayBlk.sizeof (Dom.Val.get_array_blk v) in
-      let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in
-      let mem = Dom.Mem.add_stack (Loc.of_id ret_id) empty mem in
+      let array_v = Sem.eval integer_type_widths e mem in
+      let mem = array_empty_exec ret_id array_v mem in
       match e with
       | Exp.Var id -> (
         match Dom.Mem.find_simple_alias id mem with
@@ -734,6 +738,20 @@ module StdVector = struct
         Dom.Val.set_array_length location ~length:new_size v )
 
 
+  let empty vec_exp =
+    let exec _ ~ret:(id, _) mem =
+      let deref_of_vec = deref_of vec_exp mem in
+      let array_v = Dom.Mem.find_set deref_of_vec mem in
+      let mem = array_empty_exec id array_v mem in
+      match PowLoc.is_singleton_or_more deref_of_vec with
+      | IContainer.Singleton loc ->
+          Dom.Mem.load_empty_alias id loc mem
+      | IContainer.(Empty | More) ->
+          mem
+    in
+    {exec; check= no_check}
+
+
   let push_back vec_exp elt_exp =
     let exec model_env ~ret:_ mem =
       let mem =
@@ -1120,6 +1138,7 @@ module Call = struct
         $+? any_arg $--> StdVector.constructor_copy
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "operator[]" $ capt_exp $+ capt_exp
         $--> StdVector.at
+      ; -"std" &:: "vector" < any_typ &+ any_typ >:: "empty" $ capt_exp $--> StdVector.empty
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "push_back" $ capt_exp $+ capt_exp
         $--> StdVector.push_back
       ; -"std" &:: "vector" < any_typ &+ any_typ >:: "reserve" $ any_arg $+ any_arg $--> no_model
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
index 307ae4d4a..8366ff3bb 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
@@ -107,12 +107,7 @@ codetoanalyze/cpp/bufferoverrun/std_string.cpp, to_string2_Good, 6, CONDITION_AL
 codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc::symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/this.cpp, CThis::access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this->n`,<Length trace>,Parameter `this->n`,Array declaration,Array access: Offset: this->n + 1 Size: this->n + 1]
 codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access2_Good, 2, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Array declaration,Assignment,Call,Parameter `*v->vector_elem`,Allocation: Length: 0 by call to `safe_access2` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access4_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access4` ]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_call_safe_access5_Good, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*v->vector_elem`,Array access: Offset: 0 Size: 0 by call to `safe_access5` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_data_Good, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + 4) Size: [0, +oo]]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access3_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
-codetoanalyze/cpp/bufferoverrun/vector.cpp, FP_safe_access6, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Offset trace>,Unknown value from: std::vector<int,std::allocator<int>>::empty,<Length trace>,Array declaration,Assignment,Array access: Offset: [-oo, +oo] Size: 2]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 1]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: std::vector<int,std::allocator<int>>::data,Assignment,Array access: Offset: [-oo, +oo] (⇐ [-oo, +oo] + [-oo, +oo]) Size: [0, +oo]]
@@ -121,5 +116,6 @@ codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN
 codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `idx`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
+codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/cpp/bufferoverrun/vector.cpp, simple_size_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 3 Size: 3]
 codetoanalyze/cpp/bufferoverrun/void_ptr.cpp, FP_call_casting_void_ptr_Ok, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*p`,Assignment,Array access: Offset: 14 Size: 2 by call to `casting_void_ptr` ]
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
index 5cc121694..e8e0b860a 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp
@@ -80,12 +80,12 @@ void safe_access2(std::vector<int> v) {
   }
 }
 
-void FP_call_safe_access2_Good() {
+void call_safe_access2_Good() {
   std::vector<int> v;
   safe_access2(v);
 }
 
-void FP_safe_access3_Good() {
+void safe_access3_Good() {
   std::vector<int> v;
   if (!v.empty()) {
     v[0] = 1;
@@ -98,7 +98,7 @@ void safe_access4(std::vector<int> v) {
   }
 }
 
-void FP_call_safe_access4_Good() {
+void call_safe_access4_Good() {
   std::vector<int> v;
   safe_access4(v);
 }
@@ -110,19 +110,19 @@ void safe_access5(std::vector<int> v) {
   }
 }
 
-void FP_call_safe_access5_Good() {
+void call_safe_access5_Good() {
   std::vector<int> v;
   safe_access5(v);
 }
 
-void FP_safe_access6(std::vector<int> v) {
+void safe_access6(std::vector<int> v) {
   std::vector<int> v2(2);
   v2[v.empty()];
 }
 
 void call_safe_access6_Good() {
   std::vector<int> v;
-  FP_safe_access6(v);
+  safe_access6(v);
 }
 
 void FP_data_Good() {