diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml
index d8749b0bc..1af7cef10 100644
--- a/infer/src/pulse/PulseInterproc.ml
+++ b/infer/src/pulse/PulseInterproc.ml
@@ -92,11 +92,18 @@ let fold_globals_of_stack call_loc stack call_state ~f =
           Ok call_state )
 
 
-let visit call_state ~addr_callee ~addr_hist_caller =
+let visit call_state ~pre ~addr_callee ~addr_hist_caller =
   let addr_caller = fst addr_hist_caller in
   ( match AddressMap.find_opt addr_caller call_state.rev_subst with
   | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') ->
-      raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
+      (* [addr_caller] corresponds to several values in the callee, see if that's a problem for
+         applying the pre-condition, i.e. if both values are addresses in the callee's heap, which
+         means they must be disjoint. If so, raise a contradiction, but if not then continue as it
+         just means that the callee doesn't care about the value of these variables. *)
+      if
+        BaseMemory.mem addr_callee pre.BaseDomain.heap
+        && BaseMemory.mem addr_callee' pre.BaseDomain.heap
+      then raise (Contradiction (Aliasing {addr_caller; addr_callee; addr_callee'; call_state}))
   | _ ->
       () ) ;
   if AddressSet.mem addr_callee call_state.visited then (`AlreadyVisited, call_state)
@@ -126,7 +133,7 @@ let add_call_to_trace proc_name call_location caller_history in_call =
     addresses are traversed in the process. *)
 let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_hist_caller
     call_state =
-  match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with
+  match visit call_state ~pre ~addr_callee:addr_pre ~addr_hist_caller with
   | `AlreadyVisited, call_state ->
       Ok call_state
   | `NotAlreadyVisited, call_state -> (
@@ -318,7 +325,7 @@ let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt
 let rec record_post_for_address callee_proc_name call_loc ({AbductiveDomain.pre; _} as pre_post)
     ~addr_callee ~addr_hist_caller call_state =
   L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ;
-  match visit call_state ~addr_callee ~addr_hist_caller with
+  match visit call_state ~pre:(pre :> BaseDomain.t) ~addr_callee ~addr_hist_caller with
   | `AlreadyVisited, call_state ->
       call_state
   | `NotAlreadyVisited, call_state -> (
diff --git a/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
new file mode 100644
index 000000000..782357e84
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/pulse/aliasing.cpp
@@ -0,0 +1,52 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+void ifthenderef(bool b, int* x) {
+  if (b) {
+    *x = 42;
+  }
+}
+
+void ifnotthenderef(bool b, int* x) {
+  if (!b) {
+    *x = 42;
+  }
+}
+
+void call_ifthenderef_false_null_ok() { ifthenderef(false, nullptr); }
+
+void call_ifthenderef_true_null_bad() { ifthenderef(true, nullptr); }
+
+void call_ifnotthenderef_true_null_ok() { ifnotthenderef(true, nullptr); }
+
+void call_ifnotthenderef_false_null_bad() { ifnotthenderef(false, nullptr); }
+
+// should be FN given the current "all allocated addresses are assumed
+// disjoint unless specified otherwise" but we detect the bug because
+// we don't propagate pure equalities that we discover to the heap part
+void alias_null_deref_bad(int* x, int* y) {
+  *x = 32;
+  *y = 52;
+  if (x == y) {
+    // here we have x|-> * x |-> which should be a contradiction
+    int* p = nullptr;
+    *p = 42;
+  }
+}
+
+void diverge_if_alias_ok(int* x, int* y) {
+  if (x == y) {
+    for (;;)
+      ;
+  }
+}
+
+void FP_diverge_before_null_deref_ok(int* x) {
+  diverge_if_alias_ok(x, x);
+  int* p = nullptr;
+  *p = 42;
+}
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 8f5c7bfc3..ccc57226a 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -1,3 +1,7 @@
+codetoanalyze/cpp/pulse/aliasing.cpp, FP_diverge_before_null_deref_ok, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/aliasing.cpp, alias_null_deref_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/aliasing.cpp, call_ifnotthenderef_false_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifnotthenderef` here,parameter `x` of ifnotthenderef,invalid access occurs here]
+codetoanalyze/cpp/pulse/aliasing.cpp, call_ifthenderef_true_null_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `ifthenderef` here,parameter `x` of ifthenderef,invalid access occurs here]
 codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here]
@@ -77,6 +81,7 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
+codetoanalyze/cpp/pulse/values.cpp, FP_function_empty_range_interproc_ok, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `StringRange::StringRange` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `StringRange::StringRange`,assigned,return from call to `StringRange::StringRange`,when calling `find_first_non_space` here,parameter `x` of find_first_non_space,passed as argument to `StringRange::data`,return from call to `StringRange::data`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/vector.cpp, FP_init_fill_then_push_back_loop_ok, 6, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
index 3db75d310..8feabe77d 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
@@ -111,7 +111,7 @@ void find_first_non_space(StringRange& x) {
   }
 }
 
-void function_empty_range_interproc_ok() {
+void FP_function_empty_range_interproc_ok() {
   StringRange x{};
   find_first_non_space(x);
 }