diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml
index 58d50bddb..b300206bc 100644
--- a/infer/src/checkers/PulseDomain.ml
+++ b/infer/src/checkers/PulseDomain.ml
@@ -156,14 +156,22 @@ module AttributesDomain : sig
 
   val get_invalidation : AbstractAddress.t -> astate -> Invalidation.t option
   (** None denotes a valid location *)
+
+  val std_vector_reserve : AbstractAddress.t -> astate -> astate
+
+  val is_std_vector_reserved : AbstractAddress.t -> astate -> bool
 end = struct
   module Attribute = struct
     (* OPTIM: [Invalid _] is first in the order to make queries about invalidation status more
        efficient (only need to look at the first element in the set of attributes to know if an
        address is invalid) *)
-    type t = Invalid of Invalidation.t [@@deriving compare]
+    type t = Invalid of Invalidation.t | StdVectorReserve [@@deriving compare]
 
-    let pp f = function Invalid invalidation -> Invalidation.pp f invalidation
+    let pp f = function
+      | Invalid invalidation ->
+          Invalidation.pp f invalidation
+      | StdVectorReserve ->
+          F.pp_print_string f "std::vector::reserve()"
   end
 
   module Attributes = AbstractDomain.FiniteSet (Attribute)
@@ -190,7 +198,17 @@ end = struct
        an address is invalid or not. *)
     find_opt address attribute_map
     |> Option.bind ~f:Attributes.min_elt_opt
-    |> Option.map ~f:(function Attribute.Invalid invalidation -> invalidation)
+    |> Option.bind ~f:(function Attribute.Invalid invalidation -> Some invalidation | _ -> None)
+
+
+  let std_vector_reserve address attribute_map =
+    add_attribute address Attribute.StdVectorReserve attribute_map
+
+
+  let is_std_vector_reserved address attribute_map =
+    find_opt address attribute_map
+    |> Option.value_map ~default:false ~f:(fun attributes ->
+           Attributes.mem Attribute.StdVectorReserve attributes )
 end
 
 (** the domain *)
@@ -622,5 +640,20 @@ module Operations = struct
     check_addr_access {access_expr; location} addr astate >>| mark_invalid cause addr
 end
 
+module StdVector = struct
+  open Result.Monad_infix
+
+  let is_reserved location vector_access_expr astate =
+    Operations.read location vector_access_expr astate
+    >>| fun (astate, addr) ->
+    (astate, AttributesDomain.is_std_vector_reserved addr astate.attributes)
+
+
+  let mark_reserved location vector_access_expr astate =
+    Operations.read location vector_access_expr astate
+    >>| fun (astate, addr) ->
+    {astate with attributes= AttributesDomain.std_vector_reserve addr astate.attributes}
+end
+
 include Domain
 include Operations
diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli
index 25974fd98..45eccf7e3 100644
--- a/infer/src/checkers/PulseDomain.mli
+++ b/infer/src/checkers/PulseDomain.mli
@@ -35,6 +35,12 @@ end
 
 type 'a access_result = ('a, Diagnostic.t) result
 
+module StdVector : sig
+  val is_reserved : Location.t -> AccessExpression.t -> t -> (t * bool) access_result
+
+  val mark_reserved : Location.t -> AccessExpression.t -> t -> t access_result
+end
+
 val read : Location.t -> AccessExpression.t -> t -> (t * AbstractAddress.t) access_result
 
 val read_all : Location.t -> AccessExpression.t list -> t -> t access_result
diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml
index 570d68542..6ae43890f 100644
--- a/infer/src/checkers/PulseModels.ml
+++ b/infer/src/checkers/PulseModels.ml
@@ -96,16 +96,33 @@ module StdVector = struct
         Ok (PulseDomain.havoc_var (fst ret) astate)
 
 
+  let reserve : model =
+   fun location ~ret:_ ~actuals astate ->
+    match actuals with
+    | [AccessExpression vector; _value] ->
+        PulseDomain.StdVector.mark_reserved location vector astate
+    | _ ->
+        Ok astate
+
+
   let push_back : model =
    fun location ~ret:_ ~actuals astate ->
     match actuals with
     | [AccessExpression vector; _value] ->
-        let array = to_internal_array vector in
-        (* all elements should be invalidated *)
-        let array_elements = deref_internal_array vector in
-        let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in
-        PulseDomain.invalidate invalidation location array_elements astate
-        >>= PulseDomain.havoc location array
+        PulseDomain.StdVector.is_reserved location vector astate
+        >>= fun (astate, is_reserved) ->
+        if is_reserved then
+          (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
+             (a perfect analysis would also make sure we don't exceed the reserved size) *)
+          Ok astate
+        else
+          (* simulate a re-allocation of the underlying array every time an element is added *)
+          let array = to_internal_array vector in
+          (* all elements should be invalidated *)
+          let array_elements = deref_internal_array vector in
+          let invalidation = PulseInvalidation.StdVectorPushBack (vector, location) in
+          PulseDomain.invalidate invalidation location array_elements astate
+          >>= PulseDomain.havoc location array
     | _ ->
         Ok astate
 end
@@ -115,7 +132,8 @@ module ProcNameDispatcher = struct
     let open ProcnameDispatcher.ProcName in
     make_dispatcher
       [ -"std" &:: "vector" &:: "operator[]" &--> StdVector.at
-      ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back ]
+      ; -"std" &:: "vector" &:: "push_back" &--> StdVector.push_back
+      ; -"std" &:: "vector" &:: "reserve" &--> StdVector.reserve ]
 end
 
 let builtins_dispatcher =
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 2dc839565..fd820a2bc 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -17,8 +17,6 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing3_bad, 6
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 194, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 55, column 5 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_loop_ok, 7, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 46, column 5 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 64, column 5 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
 codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
index 0019db1c4..061dd70ac 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp
@@ -31,14 +31,23 @@ void push_back_in_loop_ok(std::vector<int>& vec, std::vector<int>& vec_other) {
   }
 }
 
-void FP_reserve_then_push_back_ok(std::vector<int>& vec) {
+void reserve_then_push_back_ok(std::vector<int>& vec) {
   vec.reserve(vec.size() + 1);
   int* elt = &vec[1];
   vec.push_back(42);
   std::cout << *elt << "\n";
 }
 
-void FP_reserve_then_push_back_loop_ok(std::vector<int>& vec,
+void FN_reserve_too_small_bad() {
+  std::vector<int> vec;
+  vec.reserve(1);
+  vec.push_back(32);
+  int* elt = &vec[0];
+  vec.push_back(52);
+  std::cout << *elt << "\n";
+}
+
+void reserve_then_push_back_loop_ok(std::vector<int>& vec,
                                     std::vector<int>& vec_other) {
   vec.reserve(vec.size() + vec_other.size());
   int* elt = &vec[1];