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
@@ -69,8 +69,12 @@
     ///  `Val1` and `Val2` must be distinct.
     ///
     ///  `Val1` and `Val2` must model values of type `Type`.
+    ///
+    ///  `Val1` and `Val2` must be assigned to the same storage location in
+    ///  `Env1` and `Env2` respectively.
     virtual bool compareEquivalent(QualType Type, const Value &Val1,
-                                   const Value &Val2) {
+                                   const Environment &Env1, const Value &Val2,
+                                   const Environment &Env2) {
       // FIXME: Consider adding QualType to StructValue and removing the Type
       // argument here.
       return false;
@@ -86,8 +90,13 @@
     ///  `Val1` and `Val2` must be distinct.
     ///
     ///  `Val1`, `Val2`, and `MergedVal` must model values of type `Type`.
-    virtual bool merge(QualType Type, const Value &Val1, const Value &Val2,
-                       Value &MergedVal, Environment &Env) {
+    ///
+    ///  `Val1` and `Val2` must be assigned to the same storage location in
+    ///  `Env1` and `Env2` respectively.
+    virtual bool merge(QualType Type, const Value &Val1,
+                       const Environment &Env1, const Value &Val2,
+                       const Environment &Env2, Value &MergedVal,
+                       Environment &Env) {
       return false;
     }
   };
@@ -283,7 +292,7 @@
 
   /// Returns true if and only if the clauses that constitute the flow condition
   /// imply that `Val` is true.
-  bool flowConditionImplies(BoolValue &Val);
+  bool flowConditionImplies(BoolValue &Val) const;
 
 private:
   /// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
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
@@ -49,7 +49,9 @@
 }
 
 /// Returns true if and only if `Val1` is equivalent to `Val2`.
-static bool equivalentValues(QualType Type, Value *Val1, Value *Val2,
+static bool equivalentValues(QualType Type, Value *Val1,
+                             const Environment &Env1, Value *Val2,
+                             const Environment &Env2,
                              Environment::ValueModel &Model) {
   if (Val1 == Val2)
     return true;
@@ -60,7 +62,7 @@
     return &IndVal1->getPointeeLoc() == &IndVal2->getPointeeLoc();
   }
 
-  return Model.compareEquivalent(Type, *Val1, *Val2);
+  return Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2);
 }
 
 /// Initializes a global storage value.
@@ -105,6 +107,60 @@
   }
 }
 
+/// Returns constraints that represent the disjunction of `Constraints1` and
+/// `Constraints2`.
+///
+/// Requirements:
+///
+///  Elements of `Constraints1` and `Constraints2` must not be null.
+llvm::DenseSet<BoolValue *>
+joinConstraints(DataflowAnalysisContext *Context,
+                const llvm::DenseSet<BoolValue *> &Constraints1,
+                const llvm::DenseSet<BoolValue *> &Constraints2) {
+  llvm::DenseSet<BoolValue *> JoinedConstraints;
+
+  if (Constraints1.empty() || Constraints2.empty()) {
+    // Disjunction of empty set and non-empty set is represented as empty set.
+    return JoinedConstraints;
+  }
+
+  BoolValue *Val1 = nullptr;
+  for (BoolValue *Constraint : Constraints1) {
+    if (Constraints2.contains(Constraint)) {
+      // If a constraint is present both in `Constraints1` and `Constraints2` we
+      // can simply add it to the result to avoid unnecessarily expanding the
+      // disjunction expression.
+      JoinedConstraints.insert(Constraint);
+    } else if (Val1 == nullptr) {
+      Val1 = Constraint;
+    } else {
+      Val1 = &Context->getOrCreateConjunctionValue(*Val1, *Constraint);
+    }
+  }
+
+  BoolValue *Val2 = nullptr;
+  for (BoolValue *Constraint : Constraints2) {
+    // Common constraints are added to `JoinedConstraints` above.
+    if (Constraints1.contains(Constraint)) {
+      continue;
+    }
+    if (Val2 == nullptr) {
+      Val2 = Constraint;
+    } else {
+      Val2 = &Context->getOrCreateConjunctionValue(*Val2, *Constraint);
+    }
+  }
+
+  // `X v (X ^ Y ^ ...)` is logically equivalent to `X`. The common conditions
+  // have already been added to the result so we don't have to do anything here
+  // in the cases where only one of the values is null.
+  if (Val1 != nullptr && Val2 != nullptr)
+    JoinedConstraints.insert(
+        &Context->getOrCreateDisjunctionValue(*Val1, *Val2));
+
+  return JoinedConstraints;
+}
+
 Environment::Environment(DataflowAnalysisContext &DACtx,
                          const DeclContext &DeclCtx)
     : Environment(DACtx) {
@@ -162,7 +218,7 @@
       return false;
     assert(It->second != nullptr);
 
-    if (!equivalentValues(Loc->getType(), Val, It->second, Model))
+    if (!equivalentValues(Loc->getType(), Val, *this, It->second, Other, Model))
       return false;
   }
 
@@ -208,7 +264,8 @@
       continue;
     assert(It->second != nullptr);
 
-    if (equivalentValues(Loc->getType(), Val, It->second, Model)) {
+    if (equivalentValues(Loc->getType(), Val, *this, It->second, Other,
+                         Model)) {
       LocToVal.insert({Loc, Val});
       continue;
     }
@@ -217,12 +274,16 @@
     // `ValueModel::merge` returns false to avoid storing unneeded values in
     // `DACtx`.
     if (Value *MergedVal = createValue(Loc->getType()))
-      if (Model.merge(Loc->getType(), *Val, *It->second, *MergedVal, *this))
+      if (Model.merge(Loc->getType(), *Val, *this, *It->second, Other,
+                      *MergedVal, *this))
         LocToVal.insert({Loc, MergedVal});
   }
   if (OldLocToVal.size() != LocToVal.size())
     Effect = LatticeJoinEffect::Changed;
 
+  FlowConditionConstraints = joinConstraints(DACtx, FlowConditionConstraints,
+                                             Other.FlowConditionConstraints);
+
   return Effect;
 }
 
@@ -362,6 +423,11 @@
       Depth > MaxCompositeValueDepth)
     return nullptr;
 
+  if (Type->isBooleanType()) {
+    CreatedValuesCount++;
+    return &makeAtomicBoolValue();
+  }
+
   if (Type->isIntegerType()) {
     CreatedValuesCount++;
     return &takeOwnership(std::make_unique<IntegerValue>());
@@ -457,15 +523,15 @@
   FlowConditionConstraints.insert(&Val);
 }
 
-bool Environment::flowConditionImplies(BoolValue &Val) {
+bool Environment::flowConditionImplies(BoolValue &Val) const {
   // Returns true if and only if truth assignment of the flow condition implies
   // that `Val` is also true. We prove whether or not this property holds by
   // reducing the problem to satisfiability checking. In other words, we attempt
   // to show that assuming `Val` is false makes the constraints induced by the
   // flow condition unsatisfiable.
   llvm::DenseSet<BoolValue *> Constraints = {
-      &makeNot(Val), &getBoolLiteralValue(true),
-      &makeNot(getBoolLiteralValue(false))};
+      &DACtx->getOrCreateNegationValue(Val), &getBoolLiteralValue(true),
+      &DACtx->getOrCreateNegationValue(getBoolLiteralValue(false))};
   Constraints.insert(FlowConditionConstraints.begin(),
                      FlowConditionConstraints.end());
   return DACtx->getSolver().solve(std::move(Constraints)) ==
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
@@ -103,11 +103,9 @@
       auto &Loc = Env.createStorageLocation(*S);
       Env.setStorageLocation(*S, Loc);
       if (S->getOpcode() == BO_LAnd)
-        Env.setValue(Loc, Env.takeOwnership(std::make_unique<ConjunctionValue>(
-                              *LHSVal, *RHSVal)));
+        Env.setValue(Loc, Env.makeAnd(*LHSVal, *RHSVal));
       else
-        Env.setValue(Loc, Env.takeOwnership(std::make_unique<DisjunctionValue>(
-                              *LHSVal, *RHSVal)));
+        Env.setValue(Loc, Env.makeOr(*LHSVal, *RHSVal));
       break;
     }
     default:
@@ -269,8 +267,7 @@
 
       auto &ExprLoc = Env.createStorageLocation(*S);
       Env.setStorageLocation(*S, ExprLoc);
-      Env.setValue(ExprLoc, Env.takeOwnership(
-                                std::make_unique<NegationValue>(*SubExprVal)));
+      Env.setValue(ExprLoc, Env.makeNot(*SubExprVal));
       break;
     }
     default:
diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
--- a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
+++ b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "clang/AST/DeclCXX.h"
+#include "clang/AST/StmtVisitor.h"
 #include "clang/Analysis/Analyses/PostOrderCFGView.h"
 #include "clang/Analysis/CFG.h"
 #include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
@@ -54,6 +55,71 @@
   llvm::ArrayRef<llvm::Optional<TypeErasedDataflowAnalysisState>> BlockToState;
 };
 
+/// Returns the index of `Block` in the successors of `Pred`.
+static int blockIndexInPredecessor(const CFGBlock &Pred,
+                                   const CFGBlock &Block) {
+  auto BlockPos = llvm::find_if(
+      Pred.succs(), [&Block](const CFGBlock::AdjacentBlock &Succ) {
+        return Succ && Succ->getBlockID() == Block.getBlockID();
+      });
+  return BlockPos - Pred.succ_begin();
+}
+
+/// Extends the flow condition of an environment based on a terminator
+/// statement.
+class TerminatorVisitor : public ConstStmtVisitor<TerminatorVisitor> {
+public:
+  TerminatorVisitor(const StmtToEnvMap &StmtToEnv, Environment &Env,
+                    int BlockSuccIdx)
+      : StmtToEnv(StmtToEnv), Env(Env), BlockSuccIdx(BlockSuccIdx) {}
+
+  void VisitIfStmt(const IfStmt *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+  void VisitWhileStmt(const WhileStmt *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+  void VisitBinaryOperator(const BinaryOperator *S) {
+    auto *LHS = S->getLHS()->IgnoreParenImpCasts();
+    assert(LHS != nullptr);
+    extendFlowCondition(*LHS);
+  }
+
+  void VisitConditionalOperator(const ConditionalOperator *S) {
+    auto *Cond = S->getCond()->IgnoreParenImpCasts();
+    assert(Cond != nullptr);
+    extendFlowCondition(*Cond);
+  }
+
+private:
+  void extendFlowCondition(const Expr &Cond) {
+    // The terminator sub-expression might not be evaluated.
+    if (Env.getValue(Cond, SkipPast::None) == nullptr)
+      transfer(StmtToEnv, Cond, Env);
+
+    auto *Val =
+        cast_or_null<BoolValue>(Env.getValue(Cond, SkipPast::Reference));
+    if (Val == nullptr)
+      return;
+
+    // The condition must be inversed in one of the successors.
+    if (BlockSuccIdx == 1)
+      Val = &Env.makeNot(*Val);
+
+    Env.addToFlowCondition(*Val);
+  }
+
+  const StmtToEnvMap &StmtToEnv;
+  Environment &Env;
+  int BlockSuccIdx;
+};
+
 /// Computes the input state for a given basic block by joining the output
 /// states of its predecessors.
 ///
@@ -64,7 +130,7 @@
 ///   `llvm::None` represent basic blocks that are not evaluated yet.
 static TypeErasedDataflowAnalysisState computeBlockInputState(
     const ControlFlowContext &CFCtx,
-    llvm::ArrayRef<llvm::Optional<TypeErasedDataflowAnalysisState>> BlockStates,
+    std::vector<llvm::Optional<TypeErasedDataflowAnalysisState>> &BlockStates,
     const CFGBlock &Block, const Environment &InitEnv,
     TypeErasedDataflowAnalysis &Analysis) {
   llvm::DenseSet<const CFGBlock *> Preds;
@@ -112,13 +178,19 @@
     if (!MaybePredState.hasValue())
       continue;
 
-    const TypeErasedDataflowAnalysisState &PredState =
-        MaybePredState.getValue();
+    TypeErasedDataflowAnalysisState PredState = MaybePredState.getValue();
+    if (const Stmt *PredTerminatorStmt = Pred->getTerminatorStmt()) {
+      const StmtToEnvMapImpl StmtToEnv(CFCtx, BlockStates);
+      TerminatorVisitor(StmtToEnv, PredState.Env,
+                        blockIndexInPredecessor(*Pred, Block))
+          .Visit(PredTerminatorStmt);
+    }
+
     if (MaybeState.hasValue()) {
       Analysis.joinTypeErased(MaybeState->Lattice, PredState.Lattice);
       MaybeState->Env.join(PredState.Env, Analysis);
     } else {
-      MaybeState = PredState;
+      MaybeState = std::move(PredState);
     }
   }
   if (!MaybeState.hasValue()) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -86,6 +86,33 @@
       /*ApplyBuiltinTransfer=*/false);
 }
 
+TEST_F(TransferTest, BoolVarDecl) {
+  std::string Code = R"(
+    void target() {
+      bool Foo;
+      // [[p]]
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+                const Environment &Env = Results[0].second.Env;
+
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const StorageLocation *FooLoc =
+                    Env.getStorageLocation(*FooDecl, SkipPast::None);
+                ASSERT_TRUE(isa_and_nonnull<ScalarStorageLocation>(FooLoc));
+
+                const Value *FooVal = Env.getValue(*FooLoc);
+                EXPECT_TRUE(isa_and_nonnull<BoolValue>(FooVal));
+              });
+}
+
 TEST_F(TransferTest, IntVarDecl) {
   std::string Code = R"(
     void target() {
@@ -2035,9 +2062,7 @@
 
 TEST_F(TransferTest, AssignFromBoolConjunction) {
   std::string Code = R"(
-    void target() {
-      bool Foo = true;
-      bool Bar = true;
+    void target(bool Foo, bool Bar) {
       bool Baz = (Foo) && (Bar);
       // [[p]]
     }
@@ -2078,9 +2103,7 @@
 
 TEST_F(TransferTest, AssignFromBoolDisjunction) {
   std::string Code = R"(
-    void target() {
-      bool Foo = true;
-      bool Bar = true;
+    void target(bool Foo, bool Bar) {
       bool Baz = (Foo) || (Bar);
       // [[p]]
     }
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
@@ -336,7 +336,8 @@
   }
 
   bool compareEquivalent(QualType Type, const Value &Val1,
-                         const Value &Val2) final {
+                         const Environment &Env1, const Value &Val2,
+                         const Environment &Env2) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
@@ -346,8 +347,9 @@
            cast<StructValue>(&Val2)->getProperty("has_value");
   }
 
-  bool merge(QualType Type, const Value &Val1, const Value &Val2,
-             Value &MergedVal, Environment &Env) final {
+  bool merge(QualType Type, const Value &Val1, const Environment &Env1,
+             const Value &Val2, const Environment &Env2, Value &MergedVal,
+             Environment &Env) final {
     // Nothing to say about a value that does not model an `OptionalInt`.
     if (!Type->isRecordType() ||
         Type->getAsCXXRecordDecl()->getQualifiedNameAsString() != "OptionalInt")
@@ -559,4 +561,319 @@
               });
 }
 
+class FlowConditionTest : public Test {
+protected:
+  template <typename Matcher>
+  void runDataflow(llvm::StringRef Code, Matcher Match) {
+    ASSERT_THAT_ERROR(
+        test::checkDataflow<NoopAnalysis>(
+            Code, "target",
+            [](ASTContext &Context, Environment &Env) {
+              return NoopAnalysis(Context, true);
+            },
+            [&Match](
+                llvm::ArrayRef<
+                    std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                    Results,
+                ASTContext &ASTCtx) { Match(Results, ASTCtx); },
+            {"-fsyntax-only", "-std=c++17"}),
+        llvm::Succeeded());
+  }
+};
+
+TEST_F(FlowConditionTest, IfStmtSingleVar) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      if (Foo) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, IfStmtSingleNegatedVar) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      if (!Foo) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, WhileStmt) {
+  std::string Code = R"(
+    void target(bool Foo) {
+      while (Foo) {
+        (void)0;
+        /*[[p]]*/
+      }
+    }
+  )";
+  runDataflow(
+      Code, [](llvm::ArrayRef<
+                   std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                   Results,
+               ASTContext &ASTCtx) {
+        const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+        const Environment &Env = Results[0].second.Env;
+
+        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+      });
+}
+
+TEST_F(FlowConditionTest, Conjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Foo && Bar) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, Disjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Foo || Bar) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, NegatedConjunction) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (!(Foo && Bar)) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_FALSE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_TRUE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, DeMorgan) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (!(!Foo || !Bar)) {
+        (void)0;
+        /*[[p1]]*/
+      } else {
+        (void)1;
+        /*[[p2]]*/
+      }
+    }
+  )";
+  runDataflow(Code,
+              [](llvm::ArrayRef<
+                     std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                     Results,
+                 ASTContext &ASTCtx) {
+                const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+                ASSERT_THAT(FooDecl, NotNull());
+
+                const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
+                ASSERT_THAT(BarDecl, NotNull());
+
+                ASSERT_THAT(Results, ElementsAre(Pair("p2", _), Pair("p1", _)));
+
+                const Environment &Env1 = Results[1].second.Env;
+                auto *FooVal1 =
+                    cast<BoolValue>(Env1.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal1 =
+                    cast<BoolValue>(Env1.getValue(*BarDecl, SkipPast::None));
+                EXPECT_TRUE(Env1.flowConditionImplies(*FooVal1));
+                EXPECT_TRUE(Env1.flowConditionImplies(*BarVal1));
+
+                const Environment &Env2 = Results[0].second.Env;
+                auto *FooVal2 =
+                    cast<BoolValue>(Env2.getValue(*FooDecl, SkipPast::None));
+                auto *BarVal2 =
+                    cast<BoolValue>(Env2.getValue(*BarDecl, SkipPast::None));
+                EXPECT_FALSE(Env2.flowConditionImplies(*FooVal2));
+                EXPECT_FALSE(Env2.flowConditionImplies(*BarVal2));
+              });
+}
+
+TEST_F(FlowConditionTest, Join) {
+  std::string Code = R"(
+    void target(bool Foo, bool Bar) {
+      if (Bar) {
+        if (!Foo)
+          return;
+      } else {
+        if (!Foo)
+          return;
+      }
+      (void)0;
+      /*[[p]]*/
+    }
+  )";
+  runDataflow(
+      Code, [](llvm::ArrayRef<
+                   std::pair<std::string, DataflowAnalysisState<NoopLattice>>>
+                   Results,
+               ASTContext &ASTCtx) {
+        ASSERT_THAT(Results, ElementsAre(Pair("p", _)));
+
+        const ValueDecl *FooDecl = findValueDecl(ASTCtx, "Foo");
+        ASSERT_THAT(FooDecl, NotNull());
+
+        const Environment &Env = Results[0].second.Env;
+        auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl, SkipPast::None));
+        EXPECT_TRUE(Env.flowConditionImplies(*FooVal));
+      });
+}
+
 } // namespace