diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -153,6 +153,18 @@
     return takeOwnership(std::make_unique<AtomicBoolValue>());
   }
 
+  /// Creates a Top value for booleans. Each instance is unique and can be
+  /// assigned a distinct truth value during solving.
+  ///
+  /// FIXME: `Top iff Top` is true when both Tops are identical (by pointer
+  /// equality), but not when they are distinct values. We should improve the
+  /// implementation so that `Top iff Top` has a consistent meaning, regardless
+  /// of the identity of `Top`. Moreover, I think the meaning should be
+  /// `false`.
+  TopBoolValue &createTopBoolValue() {
+    return takeOwnership(std::make_unique<TopBoolValue>());
+  }
+
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -288,6 +288,11 @@
     return DACtx->createAtomicBoolValue();
   }
 
+  /// Returns a unique instance of boolean Top.
+  BoolValue &makeTopBoolValue() const {
+    return DACtx->createTopBoolValue();
+  }
+
   /// Returns a boolean value that represents the conjunction of `LHS` and
   /// `RHS`. Subsequent calls with the same arguments, regardless of their
   /// order, will return the same result. If the given boolean values represent
diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
--- a/clang/include/clang/Analysis/FlowSensitive/Value.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -38,6 +38,7 @@
     Struct,
 
     // Synthetic boolean values are either atomic values or logical connectives.
+    TopBool,
     AtomicBool,
     Conjunction,
     Disjunction,
@@ -82,7 +83,8 @@
   explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
 
   static bool classof(const Value *Val) {
-    return Val->getKind() == Kind::AtomicBool ||
+    return Val->getKind() == Kind::TopBool ||
+           Val->getKind() == Kind::AtomicBool ||
            Val->getKind() == Kind::Conjunction ||
            Val->getKind() == Kind::Disjunction ||
            Val->getKind() == Kind::Negation ||
@@ -91,6 +93,20 @@
   }
 };
 
+/// Models the trivially true formula, which is Top in the lattice of boolean
+/// formulas.
+///
+/// FIXME: Given the subtlety of comparison involving `TopBoolValue`, define
+/// `operator==` for `Value`.
+class TopBoolValue final : public BoolValue {
+public:
+  TopBoolValue() : BoolValue(Kind::TopBool) {}
+
+  static bool classof(const Value *Val) {
+    return Val->getKind() == Kind::TopBool;
+  }
+};
+
 /// Models an atomic boolean.
 class AtomicBoolValue : public BoolValue {
 public:
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -66,7 +66,8 @@
                              const Environment &Env1, Value *Val2,
                              const Environment &Env2,
                              Environment::ValueModel &Model) {
-  return Val1 == Val2 || areEquivalentIndirectionValues(Val1, Val2) ||
+  return Val1 == Val2 || (isa<TopBoolValue>(Val1) && isa<TopBoolValue>(Val2)) ||
+         areEquivalentIndirectionValues(Val1, Val2) ||
          Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2);
 }
 
@@ -371,7 +372,8 @@
       continue;
     assert(It->second != nullptr);
 
-    if (Val == It->second) {
+    if (Val == It->second ||
+        (isa<TopBoolValue>(Val) && isa<TopBoolValue>(It->second))) {
       JoinedEnv.LocToVal.insert({Loc, Val});
       continue;
     }
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -44,6 +44,8 @@
     return "Struct";
   case Value::Kind::AtomicBool:
     return "AtomicBool";
+  case Value::Kind::TopBool:
+    return "TopBool";
   case Value::Kind::Conjunction:
     return "Conjunction";
   case Value::Kind::Disjunction:
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -28,6 +28,7 @@
 #include "clang/Basic/OperatorKinds.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/Support/Casting.h"
+#include "llvm/Support/ErrorHandling.h"
 #include <cassert>
 #include <memory>
 #include <tuple>
@@ -46,6 +47,84 @@
   return Env.makeAtomicBoolValue();
 }
 
+// Functionally updates `V` such that any instances of `TopBool` are replaced
+// with fresh atomic bools. Note: This implementation assumes that `B` is a
+// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
+// present in the original .
+static BoolValue &unpackValue(BoolValue &V, Environment &Env);
+
+template <typename Derived, typename M>
+BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
+  auto &V = *cast<Derived>(&B);
+  BoolValue &Left = V.getLeftSubValue();
+  BoolValue &Right = V.getRightSubValue();
+  BoolValue &ULeft = unpackValue(Left, Env);
+  BoolValue &URight = unpackValue(Right, Env);
+
+  if (&ULeft == &Left && &URight == &Right)
+    return V;
+
+  return (Env.*build)(ULeft, URight);
+}
+
+static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
+  switch (V.getKind()) {
+  case Value::Kind::Integer:
+  case Value::Kind::Reference:
+  case Value::Kind::Pointer:
+  case Value::Kind::Struct:
+    llvm_unreachable("BoolValue cannot have any of these kinds.");
+
+  case Value::Kind::AtomicBool:
+    return V;
+
+  case Value::Kind::TopBool:
+    // Unpack `TopBool` into a fresh atomic bool.
+    return Env.makeAtomicBoolValue();
+
+  case Value::Kind::Negation: {
+    auto &N = *cast<NegationValue>(&V);
+    BoolValue &Sub = N.getSubVal();
+    BoolValue &USub = unpackValue(Sub, Env);
+
+    if (&USub == &Sub)
+      return V;
+    return Env.makeNot(USub);
+  }
+  case Value::Kind::Conjunction:
+    return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
+                                                   &Environment::makeAnd);
+  case Value::Kind::Disjunction:
+    return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
+                                                   &Environment::makeOr);
+  case Value::Kind::Implication:
+    return unpackBinaryBoolValue<ImplicationValue>(
+        Env, V, &Environment::makeImplication);
+  case Value::Kind::Biconditional:
+    return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
+                                                     &Environment::makeIff);
+  }
+}
+
+// Unpacks the value (if any) associated with `E` and updates `E` to the new
+// value, if any unpacking occured.
+static Value *maybeUnpackLValueExpr(const Expr &E, Environment &Env) {
+  auto *Loc = Env.getStorageLocation(E, SkipPast::Reference);
+  if (Loc == nullptr)
+    return nullptr;
+  auto *Val = Env.getValue(*Loc);
+
+  auto *B = dyn_cast_or_null<BoolValue>(Val);
+  if (B == nullptr)
+    return Val;
+
+  auto &UnpackedVal = unpackValue(*B, Env);
+  if (&UnpackedVal == Val)
+    return Val;
+  Env.setValue(*Loc, UnpackedVal);
+  return &UnpackedVal;
+}
+
 class TransferVisitor : public ConstStmtVisitor<TransferVisitor> {
 public:
   TransferVisitor(const StmtToEnvMap &StmtToEnv, Environment &Env,
@@ -222,7 +301,9 @@
     }
 
     case CK_LValueToRValue: {
-      auto *SubExprVal = Env.getValue(*SubExpr, SkipPast::Reference);
+      // When an L-value is used as an R-value, it may result in sharing, so we
+      // need to unpack any nested `Top`s.
+      auto *SubExprVal = maybeUnpackLValueExpr(*SubExpr, Env);
       if (SubExprVal == nullptr)
         break;
 
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -233,6 +233,11 @@
         UnprocessedSubVals.push(&B->getRightSubValue());
         break;
       }
+      case Value::Kind::TopBool:
+        // Nothing more to do. This `TopBool` instance has already been mapped
+        // to a fresh solver variable (`NextVar`, above) and is thereafter
+        // anonymous. The solver never sees `Top`.
+        break;
       case Value::Kind::AtomicBool: {
         Atomics[Var] = cast<AtomicBoolValue>(Val);
         break;
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -32,6 +32,19 @@
   EXPECT_NE(&X, &Y);
 }
 
+TEST_F(DataflowAnalysisContextTest,
+       CreateTopBoolValueReturnsDistinctValues) {
+  auto &X = Context.createTopBoolValue();
+  auto &Y = Context.createTopBoolValue();
+  EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
+  auto &X = Context.createTopBoolValue();
+  auto &Y = Context.createTopBoolValue();
+  EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+}
+
 TEST_F(DataflowAnalysisContextTest,
        GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
   auto &X = Context.createAtomicBoolValue();
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -10,7 +10,6 @@
 
 #include "TestingSupport.h"
 #include "clang/Analysis/FlowSensitive/Solver.h"
-#include "TestingSupport.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "gmock/gmock.h"
@@ -24,6 +23,7 @@
 using test::ConstraintContext;
 using testing::_;
 using testing::AnyOf;
+using testing::IsEmpty;
 using testing::Optional;
 using testing::Pair;
 using testing::UnorderedElementsAre;
@@ -88,6 +88,32 @@
                            Pair(Y, Solver::Result::Assignment::AssignedFalse)));
 }
 
+TEST(SolverTest, Top) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // X. Since Top is anonymous, we do not get any results in the solution.
+  expectSatisfiable(solve({X}), IsEmpty());
+}
+
+TEST(SolverTest, NegatedTop) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+
+  // !X
+  expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
+}
+
+TEST(SolverTest, DistinctTops) {
+  ConstraintContext Ctx;
+  auto X = Ctx.top();
+  auto Y = Ctx.top();
+  auto NotY = Ctx.neg(Y);
+
+  // X ^ !Y
+  expectSatisfiable(solve({X, NotY}), IsEmpty());
+}
+
 TEST(SolverTest, DoubleNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -372,6 +372,12 @@
     return Vals.back().get();
   }
 
+  // Creates an instance of the Top boolean value.
+  BoolValue *top() {
+    Vals.push_back(std::make_unique<TopBoolValue>());
+    return Vals.back().get();
+  }
+
   // Creates a boolean conjunction value.
   BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
     Vals.push_back(
diff --git a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -17,6 +17,7 @@
 #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
 #include "clang/Analysis/FlowSensitive/DataflowLattice.h"
+#include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "clang/Analysis/FlowSensitive/NoopAnalysis.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
@@ -166,7 +167,7 @@
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const auto *S = CS->getStmt();
     if (auto *C = dyn_cast<CallExpr>(S)) {
       if (auto *F = dyn_cast<FunctionDecl>(C->getCalleeDecl())) {
         E.CalledFunctions.insert(F->getNameInfo().getAsString());
@@ -310,6 +311,9 @@
 }
 
 // Models an analysis that uses flow conditions.
+//
+// FIXME: Here and below: change class to final and final methods to override,
+// since we're marking them all as final.
 class SpecialBoolAnalysis
     : public DataflowAnalysis<SpecialBoolAnalysis, NoopLattice> {
 public:
@@ -322,7 +326,7 @@
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const auto *S = CS->getStmt();
     auto SpecialBoolRecordDecl = recordDecl(hasName("SpecialBool"));
     auto HasSpecialBoolType = hasType(SpecialBoolRecordDecl);
 
@@ -468,9 +472,8 @@
 class OptionalIntAnalysis
     : public DataflowAnalysis<OptionalIntAnalysis, NoopLattice> {
 public:
-  explicit OptionalIntAnalysis(ASTContext &Context, BoolValue &HasValueTop)
-      : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context),
-        HasValueTop(HasValueTop) {}
+  explicit OptionalIntAnalysis(ASTContext &Context)
+      : DataflowAnalysis<OptionalIntAnalysis, NoopLattice>(Context) {}
 
   static NoopLattice initialElement() { return {}; }
 
@@ -478,22 +481,23 @@
     auto CS = Elt->getAs<CFGStmt>();
     if (!CS)
       return;
-    auto S = CS->getStmt();
+    const Stmt *S = CS->getStmt();
     auto OptionalIntRecordDecl = recordDecl(hasName("OptionalInt"));
     auto HasOptionalIntType = hasType(OptionalIntRecordDecl);
 
+    SmallVector<BoundNodes, 1> Matches = match(
+        stmt(anyOf(cxxConstructExpr(HasOptionalIntType).bind("construct"),
+                   cxxOperatorCallExpr(
+                       callee(cxxMethodDecl(ofClass(OptionalIntRecordDecl))))
+                       .bind("operator"))),
+        *S, getASTContext());
     if (const auto *E = selectFirst<CXXConstructExpr>(
-            "call", match(cxxConstructExpr(HasOptionalIntType).bind("call"), *S,
-                          getASTContext()))) {
+            "construct", Matches)) {
       auto &ConstructorVal = *Env.createValue(E->getType());
       ConstructorVal.setProperty("has_value", Env.getBoolLiteralValue(false));
       Env.setValue(*Env.getStorageLocation(*E, SkipPast::None), ConstructorVal);
-    } else if (const auto *E = selectFirst<CXXOperatorCallExpr>(
-                   "call",
-                   match(cxxOperatorCallExpr(callee(cxxMethodDecl(ofClass(
-                                                 OptionalIntRecordDecl))))
-                             .bind("call"),
-                         *S, getASTContext()))) {
+    } else if (const auto *E =
+                   selectFirst<CXXOperatorCallExpr>("operator", Matches)) {
       assert(E->getNumArgs() > 0);
       auto *Object = E->getArg(0);
       assert(Object != nullptr);
@@ -516,7 +520,11 @@
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
       return false;
 
-    return Val1.getProperty("has_value") == Val2.getProperty("has_value");
+    auto *Prop1  = Val1.getProperty("has_value");
+    auto *Prop2 = Val2.getProperty("has_value");
+    return Prop1 == Prop2 ||
+           (Prop1 != nullptr && Prop2 != nullptr && isa<TopBoolValue>(Prop1) &&
+            isa<TopBoolValue>(Prop2));
   }
 
   bool merge(QualType Type, const Value &Val1, const Environment &Env1,
@@ -538,11 +546,9 @@
     if (HasValue1 == HasValue2)
       MergedVal.setProperty("has_value", *HasValue1);
     else
-      MergedVal.setProperty("has_value", HasValueTop);
+      MergedVal.setProperty("has_value", MergedEnv.makeTopBoolValue());
     return true;
   }
-
-  BoolValue &HasValueTop;
 };
 
 class WideningTest : public Test {
@@ -561,11 +567,8 @@
         checkDataflow<OptionalIntAnalysis>(
             AnalysisInputs<OptionalIntAnalysis>(
                 Code, ast_matchers::hasName("target"),
-                [this](ASTContext &Context, Environment &Env) {
-                  assert(HasValueTop == nullptr);
-                  HasValueTop =
-                      &Env.takeOwnership(std::make_unique<AtomicBoolValue>());
-                  return OptionalIntAnalysis(Context, *HasValueTop);
+                [](ASTContext &Context, Environment &Env) {
+                  return OptionalIntAnalysis(Context);
                 })
                 .withASTBuildArgs({"-fsyntax-only", "-std=c++17"})
                 .withASTBuildVirtualMappedFiles(std::move(FilesContents)),
@@ -576,8 +579,6 @@
                                            &AO) { Match(Results, AO.ASTCtx); }),
         llvm::Succeeded());
   }
-
-  BoolValue *HasValueTop = nullptr;
 };
 
 TEST_F(WideningTest, JoinDistinctValuesWithDistinctProperties) {
@@ -597,8 +598,8 @@
   )";
   runDataflow(
       Code,
-      [this](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
-             ASTContext &ASTCtx) {
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         ASTContext &ASTCtx) {
         ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2", "p3"));
         const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
         const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
@@ -615,7 +616,8 @@
                   &Env1.getBoolLiteralValue(false));
         EXPECT_EQ(GetFooValue(Env2)->getProperty("has_value"),
                   &Env2.getBoolLiteralValue(true));
-        EXPECT_EQ(GetFooValue(Env3)->getProperty("has_value"), HasValueTop);
+        EXPECT_TRUE(
+            isa<TopBoolValue>(GetFooValue(Env3)->getProperty("has_value")));
       });
 }
 
@@ -1162,4 +1164,394 @@
       });
 }
 
+class TopAnalysis final : public DataflowAnalysis<TopAnalysis, NoopLattice> {
+public:
+  explicit TopAnalysis(ASTContext &Context)
+      : DataflowAnalysis<TopAnalysis, NoopLattice>(Context) {}
+
+  static NoopLattice initialElement() { return {}; }
+
+  void transfer(const CFGElement *Elt, NoopLattice &, Environment &Env) {
+    auto CS = Elt->getAs<CFGStmt>();
+    if (!CS)
+      return;
+    const Stmt *S = CS->getStmt();
+    SmallVector<BoundNodes, 1> Matches =
+        match(callExpr(callee(functionDecl(hasName("makeTop")))).bind("top"),
+              *S, getASTContext());
+    if (const auto *E = selectFirst<CallExpr>("top", Matches)) {
+      auto &Loc = Env.createStorageLocation(*E);
+      Env.setValue(Loc, Env.makeTopBoolValue());
+      Env.setStorageLocation(*E, Loc);
+    }
+  }
+
+  bool compareEquivalent(QualType Type, const Value &Val1,
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) override {
+    // Changes to a sound approximation, which allows us to test whether we can
+    // (soundly) converge for some loops.
+    return false;
+  }
+};
+
+class TopTest : public Test {
+protected:
+  template <typename Matcher>
+  void runDataflow(llvm::StringRef Code, Matcher VerifyResults) {
+    ASSERT_THAT_ERROR(
+        checkDataflow<TopAnalysis>(
+            AnalysisInputs<TopAnalysis>(
+                Code, ast_matchers::hasName("target"),
+                [](ASTContext &Context, Environment &Env) {
+                  return TopAnalysis(Context);
+                })
+                .withASTBuildArgs({"-fsyntax-only", "-std=c++17"}),
+            VerifyResults),
+        llvm::Succeeded());
+  }
+};
+
+// Tests that when Top is unused it remains Top.
+TEST_F(TopTest, UnusedTopInitializer) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target() {
+      bool Foo = makeTop();
+      /*[[p1]]*/
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal1, FooVal2);
+      });
+}
+
+// Tests that when Top is unused it remains Top. Like above, but uses the
+// assignment form rather than initialization, which uses Top as an lvalue that
+// is *not* in an rvalue position.
+TEST_F(TopTest, UnusedTopAssignment) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target() {
+      bool Foo;
+      Foo = makeTop();
+      /*[[p1]]*/
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal1, FooVal2);
+      });
+}
+
+TEST_F(TopTest, UnusedTopJoinsToTop) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = true;
+      } else {
+        Zab2 = true;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+      });
+}
+
+TEST_F(TopTest, TopUsedBeforeBranchJoinsToSameAtomicBool) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      /*[[p0]]*/
+
+      // Use `Top`.
+      bool Bar = Foo;
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = true;
+      } else {
+        Zab2 = true;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(),
+                    UnorderedElementsAre("p0", "p1", "p2"));
+        const Environment &Env0 = getEnvironmentAtAnnotation(Results, "p0");
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal0 = GetFooValue(Env0);
+        ASSERT_THAT(FooVal0, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal0))
+            << debugString(FooVal0->getKind());
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+        EXPECT_EQ(FooVal2, FooVal1);
+      });
+}
+
+TEST_F(TopTest, TopUsedInBothBranchesJoinsToAtomic) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      bool Zab1;
+      bool Zab2;
+      if (Cond) {
+        Zab1 = Foo;
+      } else {
+        Zab2 = Foo;
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<AtomicBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+      });
+}
+
+TEST_F(TopTest, TopUsedInBothBranchesWithoutPrecisionLoss) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+
+      bool Bar;
+      if (Cond) {
+        Bar = Foo;
+      } else {
+        Bar = Foo;
+      }
+      (void)0;
+      /*[[p]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p"));
+        const Environment &Env = getEnvironmentAtAnnotation(Results, "p");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        const ValueDecl *BarDecl = findValueDecl(AO.ASTCtx, "Bar");
+        ASSERT_THAT(BarDecl, NotNull());
+
+        auto *FooVal =
+            dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        ASSERT_THAT(FooVal, NotNull());
+
+        auto *BarVal =
+            dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl, SkipPast::None));
+        ASSERT_THAT(BarVal, NotNull());
+
+        EXPECT_TRUE(Env.flowConditionImplies(Env.makeIff(*FooVal, *BarVal)));
+      });
+}
+
+TEST_F(TopTest, TopUnusedBeforeLoopHeadJoinsToTop) {
+  std::string Code = R"(
+    bool makeTop();
+
+    void target(bool Cond, bool F) {
+      bool Foo = makeTop();
+      // Force a new CFG block.
+      if (F) return;
+      (void)0;
+      /*[[p1]]*/
+
+      while (Cond) {
+        // Use `Foo`.
+        bool Zab = Foo;
+        Zab = false;
+        Foo = makeTop();
+      }
+      (void)0;
+      /*[[p2]]*/
+    }
+  )";
+  runDataflow(
+      Code,
+      [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+         const AnalysisOutputs &AO) {
+        ASSERT_THAT(Results.keys(), UnorderedElementsAre("p1", "p2"));
+        const Environment &Env1 = getEnvironmentAtAnnotation(Results, "p1");
+        const Environment &Env2 = getEnvironmentAtAnnotation(Results, "p2");
+
+        const ValueDecl *FooDecl = findValueDecl(AO.ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        auto GetFooValue = [FooDecl](const Environment &Env) {
+          return Env.getValue(*FooDecl, SkipPast::None);
+        };
+
+        Value *FooVal1 = GetFooValue(Env1);
+        ASSERT_THAT(FooVal1, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal1))
+            << debugString(FooVal1->getKind());
+
+        Value *FooVal2 = GetFooValue(Env2);
+        ASSERT_THAT(FooVal2, NotNull());
+        EXPECT_TRUE(isa<TopBoolValue>(FooVal2))
+            << debugString(FooVal2->getKind());
+
+      });
+}
 } // namespace