diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 747840027..3059338d7 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -116,15 +116,12 @@ module Misc = struct
 
   let free_or_delete operation deleted_access : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we
-       currently know about the value. This is purely to avoid contributing to path explosion. *)
-    (* freeing 0 is a no-op *)
-    if PulseArithmetic.is_known_zero astate (fst deleted_access) then ok_continue astate
-    else
+    (* NOTE: freeing 0 is a no-op so we introduce a case split *)
+    let invalidation =
+      match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
+    in
+    let astates_alloc =
       let astate = PulseArithmetic.and_positive (fst deleted_access) astate in
-      let invalidation =
-        match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
-      in
       if Config.pulse_isl then
         match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with
         | Error _ as err ->
@@ -134,6 +131,9 @@ module Misc = struct
       else
         let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in
         astate
+    in
+    let astate_zero = PulseArithmetic.and_eq_int (fst deleted_access) IntLit.zero astate in
+    Ok (ContinueProgram astate_zero) :: astates_alloc
 end
 
 module C = struct
diff --git a/infer/tests/codetoanalyze/c/pulse/interprocedural.c b/infer/tests/codetoanalyze/c/pulse/interprocedural.c
index d51a3501a..a1f6ab68e 100644
--- a/infer/tests/codetoanalyze/c/pulse/interprocedural.c
+++ b/infer/tests/codetoanalyze/c/pulse/interprocedural.c
@@ -13,10 +13,10 @@ void if_freed_invalid_latent(int x, int* y) {
   }
 }
 
-void FN_call_if_freed_invalid_latent(int x) {
+void call_if_freed_invalid_latent(int x) {
   if (x > 0) {
     if_freed_invalid_latent(x, NULL);
   }
 }
 
-void FN_call_if_freed_invalid2_bad() { FN_call_if_freed_invalid_latent(7); }
+void call_if_freed_invalid2_bad() { call_if_freed_invalid_latent(7); }
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
index f8bfe2f5a..f27909aef 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp
@@ -1,5 +1,7 @@
 codetoanalyze/c/pulse/frontend.c, assign_implicit_cast_bad, 8, 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/c/pulse/frontend.c, assign_paren_bad, 8, 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/c/pulse/interprocedural.c, call_if_freed_invalid2_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `call_if_freed_invalid_latent`,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
+codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
 codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index e952a1d72..3ae733fb2 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -116,6 +116,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,is the address of a stack variable `c` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,invalid access occurs here]
 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, free_null_then_deref_bad, 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/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, 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]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
index 7ff1679d3..9188c56c3 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp
@@ -24,3 +24,9 @@ void double_free_global_bad() {
   free_global_pointer_ok();
   free_global_pointer_ok();
 }
+
+void free_null_then_deref_bad() {
+  int* x = NULL;
+  free(x);
+  *x = 1;
+}