diff --git a/nullability/BUILD b/nullability/BUILD
index 3ba5bcf..b06dd32 100644
--- a/nullability/BUILD
+++ b/nullability/BUILD
@@ -117,6 +117,7 @@
     ],
     deps = [
         ":type_nullability",
+        "@absl//absl/base:nullability",
         "@llvm-project//clang:analysis",
         "@llvm-project//clang:ast",
         "@llvm-project//clang:basic",
@@ -133,6 +134,7 @@
         "@llvm-project//clang:analysis",
         "@llvm-project//clang:ast",
         "@llvm-project//clang:basic",
+        "@llvm-project//third-party/unittest:gmock",
         "@llvm-project//third-party/unittest:gtest",
         "@llvm-project//third-party/unittest:gtest_main",
     ],
diff --git a/nullability/inference/collect_evidence.cc b/nullability/inference/collect_evidence.cc
index 5fdff82..6cf2abf 100644
--- a/nullability/inference/collect_evidence.cc
+++ b/nullability/inference/collect_evidence.cc
@@ -133,7 +133,10 @@
     std::vector<std::pair<PointerTypeNullability, Slot>> &InferableSlots,
     Evidence::Kind EvidenceKind, llvm::function_ref<EvidenceEmitter> Emit) {
   auto &A = Env.getDataflowAnalysisContext().arena();
-  auto &NotIsNull = A.makeNot(getPointerNullState(Value).IsNull);
+  auto *IsNull = getPointerNullState(Value).IsNull;
+  // If `IsNull` is top, we can't infer anything about it.
+  if (IsNull == nullptr) return;
+  auto &NotIsNull = A.makeNot(*getPointerNullState(Value).IsNull);
 
   // If the flow conditions already imply that Value is not null, then we don't
   // have any new evidence of a necessary annotation.
diff --git a/nullability/pointer_nullability.cc b/nullability/pointer_nullability.cc
index 54daf2b..8235860 100644
--- a/nullability/pointer_nullability.cc
+++ b/nullability/pointer_nullability.cc
@@ -25,6 +25,7 @@
 using dataflow::Environment;
 using dataflow::Formula;
 using dataflow::PointerValue;
+using dataflow::TopBoolValue;
 using dataflow::Value;
 
 /// The nullness information of a pointer is represented by two properties
@@ -47,17 +48,22 @@
 }
 
 PointerNullState getPointerNullState(const PointerValue &PointerVal) {
-  auto &FromNullable = *cast<BoolValue>(PointerVal.getProperty(kFromNullable));
-  auto &Null = *cast<BoolValue>(PointerVal.getProperty(kNull));
-  return {FromNullable.formula(), Null.formula()};
+  Value *FromNullableProp = PointerVal.getProperty(kFromNullable);
+  Value *NullProp = PointerVal.getProperty(kNull);
+
+  return {
+      isa<TopBoolValue>(FromNullableProp)
+          ? nullptr
+          : &cast<BoolValue>(FromNullableProp)->formula(),
+      isa<TopBoolValue>(NullProp) ? nullptr
+                                  : &cast<BoolValue>(NullProp)->formula(),
+  };
 }
 
 static bool tryCreatePointerNullState(PointerValue &PointerVal,
                                       dataflow::Arena &A,
                                       const Formula *FromNullable = nullptr,
                                       const Formula *IsNull = nullptr) {
-  // TODO: for now we assume that we have both nullability properties, or none.
-  // We'll need to relax this when properties can be independently widened away.
   if (hasPointerNullState(PointerVal)) return false;
   if (!FromNullable) FromNullable = &A.makeAtomRef(A.makeAtom());
   if (!IsNull) IsNull = &A.makeAtomRef(A.makeAtom());
@@ -77,12 +83,23 @@
     // TODO: remove this once such clauses are recognized and dropped.
     if (Source &&
         (Source->isSymbolic() || Source == NullabilityKind::NonNull)) {
-      const Formula &IsNull = getPointerNullState(PointerVal).IsNull;
-      Ctx.addInvariant(A.makeImplies(Source->isNonnull(A), A.makeNot(IsNull)));
+      if (const Formula *IsNull = getPointerNullState(PointerVal).IsNull)
+        Ctx.addInvariant(
+            A.makeImplies(Source->isNonnull(A), A.makeNot(*IsNull)));
     }
   }
 }
 
+void forgetFromNullable(dataflow::PointerValue &PointerVal,
+                        DataflowAnalysisContext &Ctx) {
+  PointerVal.setProperty(kFromNullable, Ctx.arena().makeTopValue());
+}
+
+void forgetIsNull(dataflow::PointerValue &PointerVal,
+                  DataflowAnalysisContext &Ctx) {
+  PointerVal.setProperty(kNull, Ctx.arena().makeTopValue());
+}
+
 void initNullPointer(PointerValue &PointerVal, DataflowAnalysisContext &Ctx) {
   tryCreatePointerNullState(PointerVal, Ctx.arena(),
                             /*FromNullable=*/&Ctx.arena().makeLiteral(true),
@@ -93,9 +110,18 @@
                 const dataflow::Formula *AdditionalConstraints) {
   auto &A = Env.getDataflowAnalysisContext().arena();
   auto [FromNullable, Null] = getPointerNullState(PointerVal);
-  auto *ForseeablyNull = &A.makeAnd(FromNullable, Null);
+
+  // A value is nullable if two things can be simultaneously true:
+  // - We got it from a nullable source
+  //   (values from unknown sources may be null, but are not nullable)
+  // - The value is actually null
+  //   (if a value from a nullable source was checked, it's not nullable)
+  const Formula *ForseeablyNull = &A.makeLiteral(true);
+  if (FromNullable) ForseeablyNull = &A.makeAnd(*ForseeablyNull, *FromNullable);
+  if (Null) ForseeablyNull = &A.makeAnd(*ForseeablyNull, *Null);
   if (AdditionalConstraints)
-    ForseeablyNull = &A.makeAnd(*AdditionalConstraints, *ForseeablyNull);
+    ForseeablyNull = &A.makeAnd(*ForseeablyNull, *AdditionalConstraints);
+
   return !Env.flowConditionImplies(A.makeNot(*ForseeablyNull));
 }
 
@@ -103,10 +129,11 @@
                                const dataflow::Environment &Env,
                                const dataflow::Formula *AdditionalConstraints) {
   auto &A = Env.getDataflowAnalysisContext().arena();
-  auto *Null = &getPointerNullState(PointerVal).IsNull;
-  if (AdditionalConstraints) Null = &A.makeAnd(*AdditionalConstraints, *Null);
-  if (Env.flowConditionImplies(A.makeNot(*Null)))
-    return NullabilityKind::NonNull;
+  if (auto *Null = getPointerNullState(PointerVal).IsNull) {
+    if (AdditionalConstraints) Null = &A.makeAnd(*AdditionalConstraints, *Null);
+    if (Env.flowConditionImplies(A.makeNot(*Null)))
+      return NullabilityKind::NonNull;
+  }
   return isNullable(PointerVal, Env, AdditionalConstraints)
              ? NullabilityKind::Nullable
              : NullabilityKind::Unspecified;
diff --git a/nullability/pointer_nullability.h b/nullability/pointer_nullability.h
index 8e156bb..a768650 100644
--- a/nullability/pointer_nullability.h
+++ b/nullability/pointer_nullability.h
@@ -15,6 +15,7 @@
 
 #include <optional>
 
+#include "absl/base/nullability.h"
 #include "nullability/type_nullability.h"
 #include "clang/AST/ASTContext.h"
 #include "clang/AST/ASTDumper.h"
@@ -45,11 +46,14 @@
 /// The properties representing nullness information for a pointer.
 ///
 /// We attach these properties to every PointerValue taken by an expression.
+///
+/// A null pointer for `FromNullable` or `IsNull` represents "top", i.e. we have
+/// no information on this property.
 struct PointerNullState {
   /// Did the pointer come from a known-nullable source?
-  const dataflow::Formula &FromNullable;
+  absl::Nullable<const dataflow::Formula *> FromNullable;
   /// Is the pointer's value null?
-  const dataflow::Formula &IsNull;
+  absl::Nullable<const dataflow::Formula *> IsNull;
   // These are independent: sources with unknown nullability can yield nullptr!
 };
 
@@ -79,6 +83,20 @@
     dataflow::PointerValue &PointerVal, dataflow::DataflowAnalysisContext &Ctx,
     std::optional<PointerTypeNullability> Source = std::nullopt);
 
+// Sets the `FromNullable` state of `PointerVal` to null (interpreted as "top").
+// Explicitly indicating that we don't know whether the source was nullable is a
+// form of widening that allows analysis to converge.
+// This mutates the `PointerValue`, so it should be freshly created and not have
+// been shared with other environments.
+void forgetFromNullable(dataflow::PointerValue &PointerVal,
+                        dataflow::DataflowAnalysisContext &Ctx);
+
+// Sets the `IsNull` state of `PointerVal` to null (interpreted as "top").
+// This mutates the `PointerValue`, so it should be freshly created and not have
+// been shared with other environments.
+void forgetIsNull(dataflow::PointerValue &PointerVal,
+                  dataflow::DataflowAnalysisContext &Ctx);
+
 /// Variant of initPointerNullState, where the pointer is guaranteed null.
 /// (This is flow-insensitive, but PointerTypeNullability can't represent it).
 void initNullPointer(dataflow::PointerValue &PointerVal,
diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index 337bffd..1e34a58 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -27,6 +27,7 @@
 #include "clang/Analysis/FlowSensitive/Arena.h"
 #include "clang/Analysis/FlowSensitive/CFGMatchSwitch.h"
 #include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/StorageLocation.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
@@ -40,6 +41,7 @@
 using ast_matchers::MatchFinder;
 using dataflow::BoolValue;
 using dataflow::CFGMatchSwitchBuilder;
+using dataflow::DataflowAnalysisContext;
 using dataflow::Environment;
 using dataflow::Formula;
 using dataflow::PointerValue;
@@ -308,24 +310,32 @@
   if (!LHS || !RHS) return;
   if (!hasPointerNullState(*LHS) || !hasPointerNullState(*RHS)) return;
 
-  auto &LHSNull = getPointerNullState(*LHS).IsNull;
-  auto &RHSNull = getPointerNullState(*RHS).IsNull;
+  auto *LHSNull = getPointerNullState(*LHS).IsNull;
+  auto *RHSNull = getPointerNullState(*RHS).IsNull;
+
+  // If the null state of either pointer is "top", the result of the comparison
+  // is a top bool, and we don't have any knowledge we can add to the flow
+  // condition.
+  if (LHSNull == nullptr || RHSNull == nullptr) {
+    State.Env.setValue(*BinaryOp, A.makeTopValue());
+    return;
+  }
 
   // Special case: Are we comparing against `nullptr`?
   // We can avoid modifying the flow condition in this case and simply propagate
   // the nullability of the other operand (potentially with a negation).
-  if (&LHSNull == &A.makeLiteral(true)) {
+  if (LHSNull == &A.makeLiteral(true)) {
     if (BinaryOp->getOpcode() == BO_EQ)
-      State.Env.setValue(*BinaryOp, A.makeBoolValue(RHSNull));
+      State.Env.setValue(*BinaryOp, A.makeBoolValue(*RHSNull));
     else
-      State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(RHSNull)));
+      State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(*RHSNull)));
     return;
   }
-  if (&RHSNull == &A.makeLiteral(true)) {
+  if (RHSNull == &A.makeLiteral(true)) {
     if (BinaryOp->getOpcode() == BO_EQ)
-      State.Env.setValue(*BinaryOp, A.makeBoolValue(LHSNull));
+      State.Env.setValue(*BinaryOp, A.makeBoolValue(*LHSNull));
     else
-      State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(LHSNull)));
+      State.Env.setValue(*BinaryOp, A.makeBoolValue(A.makeNot(*LHSNull)));
     return;
   }
 
@@ -344,13 +354,13 @@
 
   // nullptr == nullptr
   State.Env.addToFlowCondition(
-      A.makeImplies(A.makeAnd(LHSNull, RHSNull), PointerEQ));
+      A.makeImplies(A.makeAnd(*LHSNull, *RHSNull), PointerEQ));
   // nullptr != notnull
   State.Env.addToFlowCondition(
-      A.makeImplies(A.makeAnd(LHSNull, A.makeNot(RHSNull)), PointerNE));
+      A.makeImplies(A.makeAnd(*LHSNull, A.makeNot(*RHSNull)), PointerNE));
   // notnull != nullptr
   State.Env.addToFlowCondition(
-      A.makeImplies(A.makeAnd(A.makeNot(LHSNull), RHSNull), PointerNE));
+      A.makeImplies(A.makeAnd(A.makeNot(*LHSNull), *RHSNull), PointerNE));
 }
 
 void transferFlowSensitiveNullCheckImplicitCastPtrToBool(
@@ -362,7 +372,11 @@
   if (!PointerVal) return;
 
   auto Nullability = getPointerNullState(*PointerVal);
-  State.Env.setValue(*CastExpr, A.makeBoolValue(A.makeNot(Nullability.IsNull)));
+  if (Nullability.IsNull != nullptr)
+    State.Env.setValue(*CastExpr,
+                       A.makeBoolValue(A.makeNot(*Nullability.IsNull)));
+  else
+    State.Env.setValue(*CastExpr, A.makeTopValue());
 }
 
 void initializeOutputParameter(const Expr *Arg, dataflow::Environment &Env,
@@ -878,15 +892,17 @@
   FlowSensitiveTransferer(Elt, getASTContext(), State);
 }
 
-static const Formula &mergeFormulas(const Formula &Bool1,
+static const Formula *mergeFormulas(const Formula *Bool1,
                                     const Environment &Env1,
-                                    const Formula &Bool2,
+                                    const Formula *Bool2,
                                     const Environment &Env2,
                                     Environment &MergedEnv) {
-  if (&Bool1 == &Bool2) {
+  if (Bool1 == Bool2) {
     return Bool1;
   }
 
+  if (Bool1 == nullptr || Bool2 == nullptr) return nullptr;
+
   auto &A = MergedEnv.arena();
   auto &MergedBool = A.makeAtomRef(A.makeAtom());
 
@@ -895,10 +911,10 @@
   // path taken - this simplifies the flow condition tracked in `MergedEnv`.
   // Otherwise, information about which path was taken is used to associate
   // `MergedBool` with `Bool1` and `Bool2`.
-  if (Env1.flowConditionImplies(Bool1) && Env2.flowConditionImplies(Bool2)) {
+  if (Env1.flowConditionImplies(*Bool1) && Env2.flowConditionImplies(*Bool2)) {
     MergedEnv.addToFlowCondition(MergedBool);
-  } else if (Env1.flowConditionImplies(A.makeNot(Bool1)) &&
-             Env2.flowConditionImplies(A.makeNot(Bool2))) {
+  } else if (Env1.flowConditionImplies(A.makeNot(*Bool1)) &&
+             Env2.flowConditionImplies(A.makeNot(*Bool2))) {
     MergedEnv.addToFlowCondition(A.makeNot(MergedBool));
   } else {
     // TODO(b/233582219): Flow conditions are not necessarily mutually
@@ -907,10 +923,10 @@
     auto FC1 = Env1.getFlowConditionToken();
     auto FC2 = Env2.getFlowConditionToken();
     MergedEnv.addToFlowCondition(A.makeOr(
-        A.makeAnd(A.makeAtomRef(FC1), A.makeEquals(MergedBool, Bool1)),
-        A.makeAnd(A.makeAtomRef(FC2), A.makeEquals(MergedBool, Bool2))));
+        A.makeAnd(A.makeAtomRef(FC1), A.makeEquals(MergedBool, *Bool1)),
+        A.makeAnd(A.makeAtomRef(FC2), A.makeEquals(MergedBool, *Bool2))));
   }
-  return MergedBool;
+  return &MergedBool;
 }
 
 bool PointerNullabilityAnalysis::merge(QualType Type, const Value &Val1,
@@ -928,22 +944,35 @@
     return false;
   }
 
+  auto &MergedPointerVal = cast<PointerValue>(MergedVal);
+  DataflowAnalysisContext &Ctx = MergedEnv.getDataflowAnalysisContext();
+  auto &A = MergedEnv.arena();
+
   auto Nullability1 = getPointerNullState(cast<PointerValue>(Val1));
   auto Nullability2 = getPointerNullState(cast<PointerValue>(Val2));
 
-  auto &FromNullable =
-      mergeFormulas(Nullability1.FromNullable, Env1, Nullability2.FromNullable,
-                    Env2, MergedEnv);
-  auto &Null = mergeFormulas(Nullability1.IsNull, Env1, Nullability2.IsNull,
-                             Env2, MergedEnv);
+  // Initialize `MergedPointerVal`'s nullability properties with atoms. These
+  // are potentially replaced with "top" below.
+  assert(!hasPointerNullState(MergedPointerVal));
+  initPointerNullState(MergedPointerVal, Ctx);
+  auto MergedNullability = getPointerNullState(MergedPointerVal);
+  assert(MergedNullability.FromNullable != nullptr);
+  assert(MergedNullability.IsNull != nullptr);
 
-  initPointerNullState(cast<PointerValue>(MergedVal),
-                       MergedEnv.getDataflowAnalysisContext());
-  auto MergedNullability = getPointerNullState(cast<PointerValue>(MergedVal));
-  auto &A = MergedEnv.arena();
-  MergedEnv.addToFlowCondition(
-      A.makeEquals(MergedNullability.FromNullable, FromNullable));
-  MergedEnv.addToFlowCondition(A.makeEquals(MergedNullability.IsNull, Null));
+  if (auto *FromNullable =
+          mergeFormulas(Nullability1.FromNullable, Env1,
+                        Nullability2.FromNullable, Env2, MergedEnv))
+    MergedEnv.addToFlowCondition(
+        A.makeEquals(*MergedNullability.FromNullable, *FromNullable));
+  else
+    forgetFromNullable(MergedPointerVal, Ctx);
+
+  if (auto *Null = mergeFormulas(Nullability1.IsNull, Env1, Nullability2.IsNull,
+                                 Env2, MergedEnv))
+    MergedEnv.addToFlowCondition(
+        A.makeEquals(*MergedNullability.IsNull, *Null));
+  else
+    forgetIsNull(MergedPointerVal, Ctx);
 
   return true;
 }
diff --git a/nullability/pointer_nullability_analysis_test.cc b/nullability/pointer_nullability_analysis_test.cc
index 61eb15d..1bc46f8 100644
--- a/nullability/pointer_nullability_analysis_test.cc
+++ b/nullability/pointer_nullability_analysis_test.cc
@@ -20,7 +20,6 @@
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "clang/Basic/LLVM.h"
 #include "clang/Testing/TestAST.h"
-#include "llvm/Support/Error.h"
 #include "third_party/llvm/llvm-project/third-party/unittest/googletest/include/gtest/gtest.h"
 
 namespace clang::tidy::nullability {
@@ -72,18 +71,20 @@
       dyn_cast_or_null<dataflow::PointerValue>(ExitState.Env.getReturnValue());
   ASSERT_NE(Ret, nullptr);
   auto State = getPointerNullState(*Ret);
+  ASSERT_NE(State.FromNullable, nullptr);
+  ASSERT_NE(State.IsNull, nullptr);
 
   // The param nullability hasn't been fixed.
   EXPECT_EQ(std::nullopt, evaluate(PN.isNonnull(A), ExitState.Env));
   EXPECT_EQ(std::nullopt, evaluate(PN.isNullable(A), ExitState.Env));
   // Nor has the the nullability of the returned pointer.
-  EXPECT_EQ(std::nullopt, evaluate(State.FromNullable, ExitState.Env));
-  EXPECT_EQ(std::nullopt, evaluate(State.IsNull, ExitState.Env));
+  EXPECT_EQ(std::nullopt, evaluate(*State.FromNullable, ExitState.Env));
+  EXPECT_EQ(std::nullopt, evaluate(*State.IsNull, ExitState.Env));
   // However, the two are linked as expected.
   EXPECT_EQ(true,
-            evaluate(A.makeImplies(PN.isNonnull(A), A.makeNot(State.IsNull)),
+            evaluate(A.makeImplies(PN.isNonnull(A), A.makeNot(*State.IsNull)),
                      ExitState.Env));
-  EXPECT_EQ(true, evaluate(A.makeEquals(PN.isNullable(A), State.FromNullable),
+  EXPECT_EQ(true, evaluate(A.makeEquals(PN.isNullable(A), *State.FromNullable),
                            ExitState.Env));
 }
 
diff --git a/nullability/pointer_nullability_test.cc b/nullability/pointer_nullability_test.cc
index 3e54939..9060082 100644
--- a/nullability/pointer_nullability_test.cc
+++ b/nullability/pointer_nullability_test.cc
@@ -47,22 +47,26 @@
   {
     auto &NullableButNotNull = makePointer(NullabilityKind::Nullable);
     EXPECT_TRUE(isNullable(NullableButNotNull, Env));
-    Env.addToFlowCondition(
-        A.makeNot(getPointerNullState(NullableButNotNull).IsNull));
+    auto *IsNull = getPointerNullState(NullableButNotNull).IsNull;
+    ASSERT_NE(IsNull, nullptr);
+    Env.addToFlowCondition(A.makeNot(*IsNull));
     EXPECT_FALSE(isNullable(NullableButNotNull, Env));
   }
 
   {
     auto &NullableAndNull = makePointer(NullabilityKind::Nullable);
-    Env.addToFlowCondition(getPointerNullState(NullableAndNull).IsNull);
+    auto *IsNull = getPointerNullState(NullableAndNull).IsNull;
+    ASSERT_NE(IsNull, nullptr);
+    Env.addToFlowCondition(*IsNull);
     EXPECT_TRUE(isNullable(NullableAndNull, Env));
   }
 
   {
     auto &NonnullAndNotNull = makePointer(NullabilityKind::NonNull);
     EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
-    Env.addToFlowCondition(
-        A.makeNot(getPointerNullState(NonnullAndNotNull).IsNull));
+    auto *IsNull = getPointerNullState(NonnullAndNotNull).IsNull;
+    ASSERT_NE(IsNull, nullptr);
+    Env.addToFlowCondition(A.makeNot(*IsNull));
     EXPECT_FALSE(isNullable(NonnullAndNotNull, Env));
   }
 
@@ -71,7 +75,9 @@
     // but is dynamically discovered to be definitely null, we still don't
     // consider it nullable.
     auto &NonnullAndNull = makePointer(NullabilityKind::NonNull);
-    Env.addToFlowCondition(getPointerNullState(NonnullAndNull).IsNull);
+    auto *IsNull = getPointerNullState(NonnullAndNull).IsNull;
+    ASSERT_NE(IsNull, nullptr);
+    Env.addToFlowCondition(*IsNull);
     EXPECT_FALSE(isNullable(NonnullAndNull, Env));
   }
 }
@@ -79,16 +85,35 @@
 TEST_F(NullabilityPropertiesTest, IsNullableAdditionalConstraints) {
   auto &P = makePointer(NullabilityKind::Nullable);
   EXPECT_TRUE(isNullable(P, Env));
-  auto *NotNull = &DACtx.arena().makeNot(getPointerNullState(P).IsNull);
+  auto *IsNull = getPointerNullState(P).IsNull;
+  ASSERT_NE(IsNull, nullptr);
+  auto *NotNull = &DACtx.arena().makeNot(*IsNull);
   EXPECT_FALSE(isNullable(P, Env, NotNull));
 }
 
 TEST_F(NullabilityPropertiesTest, GetNullabilityAdditionalConstraints) {
   auto &P = makePointer(NullabilityKind::Nullable);
   EXPECT_EQ(getNullability(P, Env), NullabilityKind::Nullable);
-  auto *NotNull = &DACtx.arena().makeNot(getPointerNullState(P).IsNull);
+  auto *IsNull = getPointerNullState(P).IsNull;
+  ASSERT_NE(IsNull, nullptr);
+  auto *NotNull = &DACtx.arena().makeNot(*IsNull);
   EXPECT_EQ(getNullability(P, Env, NotNull), NullabilityKind::NonNull);
 }
 
+TEST_F(NullabilityPropertiesTest, InitNullabilityPropertiesWithTop) {
+  auto &P = Env.create<dataflow::PointerValue>(
+      DACtx.createStorageLocation(QualType()));
+
+  initPointerNullState(P, DACtx);
+  ASSERT_NE(getPointerNullState(P).FromNullable, nullptr);
+  ASSERT_NE(getPointerNullState(P).IsNull, nullptr);
+
+  forgetFromNullable(P, DACtx);
+  ASSERT_EQ(getPointerNullState(P).FromNullable, nullptr);
+
+  forgetIsNull(P, DACtx);
+  ASSERT_EQ(getPointerNullState(P).IsNull, nullptr);
+}
+
 }  // namespace
 }  // namespace clang::tidy::nullability