diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index 4282897ae..85a4c1eb8 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -351,13 +351,6 @@ let sigma_gen_free_vars sigma = ISequence.gen_sequence_list sigma ~f:Sil.hpred_g
 
 let sigma_free_vars sigma = Sequence.Generator.run (sigma_gen_free_vars sigma)
 
-(** Find free variables in the footprint part of the prop *)
-let footprint_gen_free_vars {sigma_fp; pi_fp} =
-  Sequence.Generator.(sigma_gen_free_vars sigma_fp >>= fun () -> pi_gen_free_vars pi_fp)
-
-
-let footprint_free_vars prop = Sequence.Generator.run (footprint_gen_free_vars prop)
-
 let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} =
   let open Sequence.Generator in
   sigma_gen_free_vars sigma
@@ -370,6 +363,16 @@ let gen_free_vars {sigma; sigma_fp; sub; pi; pi_fp} =
 
 let free_vars prop = Sequence.Generator.run (gen_free_vars prop)
 
+let seq_max_stamp predicate seq =
+  seq |> Sequence.filter ~f:predicate |> Sequence.map ~f:Ident.get_stamp
+  |> Sequence.max_elt ~compare:Int.compare
+  |> Option.value ~default:0
+
+
+let all_true _ = true
+
+let max_stamp ?(f = all_true) prop = seq_max_stamp f (free_vars prop)
+
 let exposed_gen_free_vars prop = gen_free_vars (unsafe_cast_to_normal prop)
 
 let sorted_gen_free_vars prop = exposed_gen_free_vars (expose_sorted prop)
@@ -2490,10 +2493,6 @@ let prop_iter_footprint_gen_free_vars {pit_sigma_fp; pit_pi_fp} =
   Sequence.Generator.(sigma_gen_free_vars pit_sigma_fp >>= fun () -> pi_gen_free_vars pit_pi_fp)
 
 
-let prop_iter_footprint_free_vars iter =
-  Sequence.Generator.run (prop_iter_footprint_gen_free_vars iter)
-
-
 (** Find fav of the iterator *)
 let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_curr} as iter) =
   let open Sequence.Generator in
@@ -2512,6 +2511,8 @@ let prop_iter_gen_free_vars ({pit_sub; pit_pi; pit_newpi; pit_old; pit_new; pit_
 
 let prop_iter_free_vars iter = Sequence.Generator.run (prop_iter_gen_free_vars iter)
 
+let prop_iter_max_stamp ?(f = all_true) iter = seq_max_stamp f (prop_iter_free_vars iter)
+
 (** Extract the sigma part of the footprint *)
 let prop_iter_get_footprint_sigma iter = iter.pit_sigma_fp
 
diff --git a/infer/src/biabduction/Prop.mli b/infer/src/biabduction/Prop.mli
index 7b57ba61b..d0069db2d 100644
--- a/infer/src/biabduction/Prop.mli
+++ b/infer/src/biabduction/Prop.mli
@@ -82,6 +82,8 @@ val d_prop : 'a t -> unit
 
 val d_proplist_with_typ : 'a t list -> unit
 
+val max_stamp : ?f:(Ident.t -> bool) -> normal t -> int
+
 val pi_free_vars : pi -> Ident.t Sequence.t
 
 val sigma_free_vars : sigma -> Ident.t Sequence.t
@@ -90,8 +92,6 @@ val free_vars : normal t -> Ident.t Sequence.t
 
 val gen_free_vars : normal t -> (unit, Ident.t) Sequence.Generator.t
 
-val footprint_free_vars : normal t -> Ident.t Sequence.t
-
 val sorted_gen_free_vars : sorted t -> (unit, Ident.t) Sequence.Generator.t
 
 val non_pure_free_vars : normal t -> Ident.t Sequence.t
@@ -295,11 +295,8 @@ val prop_iter_update_current : 'a prop_iter -> hpred -> 'a prop_iter
 val prop_iter_prev_then_insert : 'a prop_iter -> hpred -> 'a prop_iter
 (** Insert before the current element of the iterator. *)
 
-val prop_iter_footprint_free_vars : 'a prop_iter -> Ident.t Sequence.t
-(** Find fav of the footprint part of the iterator *)
-
-val prop_iter_free_vars : 'a prop_iter -> Ident.t Sequence.t
-(** Find fav of the iterator *)
+val prop_iter_max_stamp : ?f:(Ident.t -> bool) -> 'a prop_iter -> int
+(** Find the maximum stamp of a free variable of a certain kind. *)
 
 val prop_iter_get_footprint_sigma : 'a prop_iter -> hpred list
 (** Extract the sigma part of the footprint *)
diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml
index 700d2d6bc..4d7569a52 100644
--- a/infer/src/biabduction/Rearrange.ml
+++ b/infer/src/biabduction/Rearrange.ml
@@ -522,8 +522,6 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
   check_offset se offset
 
 
-let id_max_stamp curr_max id = max curr_max (Ident.get_stamp id)
-
 (** [prop_iter_extend_ptsto iter lexp] extends the current psto
     predicate in [iter] with enough fields to follow the path in
     [lexp] -- field splitting model. It also materializes all
@@ -534,7 +532,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
     Sil.d_exp lexp ;
     L.d_ln () ) ;
   let offset = Sil.exp_get_offsets lexp in
-  let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in
+  let max_stamp = Prop.prop_iter_max_stamp iter in
   let extend_footprint_pred = function
     | Sil.Hpointsto (e, se, te) ->
         let atoms_se_te_list =
@@ -677,7 +675,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
     that [root(lexp): typ] is the current hpred of the iterator. typ
     is the type of the root of lexp. *)
 let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
-  let max_stamp = Prop.footprint_free_vars prop |> Sequence.fold ~init:0 ~f:id_max_stamp in
+  let max_stamp = Prop.max_stamp ~f:Ident.is_footprint prop in
   let ptsto, ptsto_foot, atoms =
     mk_ptsto_exp_footprint pname tenv prop (lexp, typ) (ref max_stamp) inst
   in
@@ -1046,9 +1044,7 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst =
     L.d_str "typ:" ;
     Typ.d_full typ ;
     L.d_ln () ) ;
-  let max_stamp =
-    Prop.prop_iter_footprint_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp
-  in
+  let max_stamp = Prop.prop_iter_max_stamp ~f:Ident.is_footprint iter in
   let ptsto, ptsto_foot, atoms =
     mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) (ref max_stamp) inst
   in
@@ -1127,7 +1123,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
       check_field_splitting () ;
       match Prop.prop_iter_current tenv iter with
       | Sil.Hpointsto (e, se, te), offset ->
-          let max_stamp = Prop.prop_iter_free_vars iter |> Sequence.fold ~init:0 ~f:id_max_stamp in
+          let max_stamp = Prop.prop_iter_max_stamp iter in
           let atoms_se_te_list =
             strexp_extend_values pname tenv orig_prop false Ident.kprimed (ref max_stamp) se te
               offset inst
diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp
index 224380184..5e2935d53 100644
--- a/infer/tests/codetoanalyze/c/biabduction/issues.exp
+++ b/infer/tests/codetoanalyze/c/biabduction/issues.exp
@@ -4,5 +4,6 @@ codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, B1, ERROR, [sta
 codetoanalyze/c/biabduction/example.c, global_addr_alias_bad, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure global_addr_alias_bad(),Taking true branch]
 codetoanalyze/c/biabduction/example.c, local_addr_noalias_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure local_addr_noalias_bad(),Taking true branch]
 codetoanalyze/c/biabduction/example.c, null_dereference_following_function_pointer_call_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure null_dereference_following_function_pointer_call_bad(),Skipping __function_pointer__(): unresolved function pointer]
+codetoanalyze/c/biabduction/nulluse.c, fail, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure fail(),Taking true branch]
 codetoanalyze/c/biabduction/shift.c, return_null_deref1_bad, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure return_null_deref1_bad(),start of procedure return_depends_on_lshift(),Taking true branch,return from a call to return_depends_on_lshift]
 codetoanalyze/c/biabduction/shift.c, return_null_deref2_bad, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure return_null_deref2_bad(),start of procedure return_depends_on_rshift(),Taking true branch,return from a call to return_depends_on_rshift]
diff --git a/infer/tests/codetoanalyze/c/biabduction/nulluse.c b/infer/tests/codetoanalyze/c/biabduction/nulluse.c
new file mode 100644
index 000000000..200ec4e46
--- /dev/null
+++ b/infer/tests/codetoanalyze/c/biabduction/nulluse.c
@@ -0,0 +1,41 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+void (*global)(void**);
+
+struct T {
+  void (*go)();
+};
+
+struct S {
+  struct T* t;
+  void* x;
+};
+
+void doit(void** x) {
+  if (global != 0) {
+    global(x);
+  }
+}
+
+void f(struct S* s) {
+  if (s == 0)
+    return;
+  doit(&s->x);
+  if (s->t->go) { // should *not* give NULL_TEST_AFTER_DEREFERENCE
+    s->t->go();
+  }
+}
+
+void fail(int* x) {
+  if (x == 0) {
+    *x = 1; // should give NULL_DEREFERENCE
+  }
+}
+
+int main() {}