diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index e5e5b8f0f..b964b56a9 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -1572,6 +1572,7 @@ module ProcNameDispatcher = struct
           <>$ capt_exp
           $--> Misc.alloc_no_leak_not_null ~desc:"new"
         ; +BuiltinDecl.(match_builtin __placement_new) &++> Cplusplus.placement_new
+        ; -"random" <>$$--> Misc.nondet ~fn_name:"random"
         ; +BuiltinDecl.(match_builtin objc_cpp_throw) <>--> Misc.early_exit
         ; +BuiltinDecl.(match_builtin __cast)
           <>$ capt_arg_payload $+...$--> Misc.id_first_arg ~desc:"cast"
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
index fec0414ab..4f5d74325 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp
@@ -29,6 +29,8 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_
 codetoanalyze/c/pulse/memory_leak.c, return_malloc_deref_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
+codetoanalyze/c/pulse/nullptr.c, FNlatent_random_modelled_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, FP_arithmetic_weakness_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
@@ -38,6 +40,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, random_non_functional_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,parameter `z` of several_dereferences_ok,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
index d3caea2a8..8f6266e19 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp-isl
@@ -32,6 +32,8 @@ codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_
 codetoanalyze/c/pulse/memory_leak.c, return_malloc_deref_bad, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
+codetoanalyze/c/pulse/nullptr.c, FNlatent_random_modelled_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, FP_arithmetic_weakness_ok, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
@@ -41,6 +43,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, random_non_functional_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, report_correct_error_among_multiple_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,when calling `several_dereferences_ok` here,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, unknown_from_parameters_latent, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, unknown_with_different_values_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c
index 5733b377a..b5fee2679 100644
--- a/infer/tests/codetoanalyze/c/pulse/nullptr.c
+++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c
@@ -163,3 +163,30 @@ void unknown_from_parameters_latent(int x) {
     *p = 42;
   }
 }
+
+// is pruned away without the model
+void random_non_functional_bad() {
+  if (random() != random()) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+// quantifier elimination not powerful enough to discard [\exists v. y = v] in
+// the pruned part
+void FNlatent_random_modelled_bad(int y) {
+  int x = random();
+  if (x == y) {
+    int* p = NULL;
+    *p = 42;
+  }
+}
+
+void FP_arithmetic_weakness_ok() {
+  int x = random();
+  int y = random();
+  if (x < y && x > y) {
+    int* p = NULL;
+    *p = 42;
+  }
+}