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
@@ -215,7 +215,9 @@
   /// conditions identified by `FirstToken` and `SecondToken`, and returns its
   /// token.
   AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
-                                      AtomicBoolValue &SecondToken);
+                                      AtomicBoolValue &SecondToken,
+                                      AtomicBoolValue &TookFirstBranchToken,
+                                      AtomicBoolValue &TookSecondBranchToken);
 
   // FIXME: This function returns the flow condition expressed directly as its
   // constraints: (C1 AND C2 AND ...). This differs from the general approach in
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -143,14 +143,23 @@
   return ForkToken;
 }
 
-AtomicBoolValue &
-DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
-                                            AtomicBoolValue &SecondToken) {
+AtomicBoolValue &DataflowAnalysisContext::joinFlowConditions(
+    AtomicBoolValue &FirstToken, AtomicBoolValue &SecondToken,
+    AtomicBoolValue &TookFirstBranchToken,
+    AtomicBoolValue &TookSecondBranchToken) {
   auto &Token = makeFlowConditionToken();
+  FlowConditionDeps[&Token].insert(&TookFirstBranchToken);
+  FlowConditionDeps[&Token].insert(&TookSecondBranchToken);
+  addFlowConditionConstraint(
+      Token, getOrCreateDisjunction(
+                 getOrCreateNegation(TookFirstBranchToken),
+                 getOrCreateNegation(TookSecondBranchToken)));
   FlowConditionDeps[&Token].insert(&FirstToken);
   FlowConditionDeps[&Token].insert(&SecondToken);
-  addFlowConditionConstraint(Token,
-                             getOrCreateDisjunction(FirstToken, SecondToken));
+  addFlowConditionConstraint(
+      Token, getOrCreateDisjunction(
+                 getOrCreateConjunction(TookFirstBranchToken, FirstToken),
+                 getOrCreateConjunction(TookSecondBranchToken, SecondToken)));
   return Token;
 }
 
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
@@ -79,19 +79,18 @@
                                   const Environment &Env1, Value *Val2,
                                   const Environment &Env2,
                                   Environment &MergedEnv,
-                                  Environment::ValueModel &Model) {
+                                  Environment::ValueModel &Model,
+                                  AtomicBoolValue &TookLeftBranchToken,
+                                  AtomicBoolValue &TookRightBranchToken) {
   // Join distinct boolean values preserving information about the constraints
   // in the respective path conditions.
-  //
-  // FIXME: Does not work for backedges, since the two (or more) paths will not
-  // have mutually exclusive conditions.
   if (auto *Expr1 = dyn_cast<BoolValue>(Val1)) {
     auto *Expr2 = cast<BoolValue>(Val2);
     auto &MergedVal = MergedEnv.makeAtomicBoolValue();
     MergedEnv.addToFlowCondition(MergedEnv.makeOr(
-        MergedEnv.makeAnd(Env1.getFlowConditionToken(),
+        MergedEnv.makeAnd(TookLeftBranchToken,
                           MergedEnv.makeIff(MergedVal, *Expr1)),
-        MergedEnv.makeAnd(Env2.getFlowConditionToken(),
+        MergedEnv.makeAnd(TookRightBranchToken,
                           MergedEnv.makeIff(MergedVal, *Expr2))));
     return &MergedVal;
   }
@@ -253,9 +252,13 @@
   if (MemberLocToStruct.size() != JoinedEnv.MemberLocToStruct.size())
     Effect = LatticeJoinEffect::Changed;
 
+  auto &TookLeftBranchToken = DACtx->createAtomicBoolValue();
+  auto &TookRightBranchToken = DACtx->createAtomicBoolValue();
+
   // FIXME: set `Effect` as needed.
-  JoinedEnv.FlowConditionToken = &DACtx->joinFlowConditions(
-      *FlowConditionToken, *Other.FlowConditionToken);
+  JoinedEnv.FlowConditionToken =
+      &DACtx->joinFlowConditions(*FlowConditionToken, *Other.FlowConditionToken,
+                                 TookLeftBranchToken, TookRightBranchToken);
 
   for (auto &Entry : LocToVal) {
     const StorageLocation *Loc = Entry.first;
@@ -275,7 +278,8 @@
     }
 
     if (Value *MergedVal = mergeDistinctValues(
-            Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model))
+            Loc->getType(), Val, *this, It->second, Other, JoinedEnv, Model,
+            TookLeftBranchToken, TookRightBranchToken))
       JoinedEnv.LocToVal.insert({Loc, MergedVal});
   }
   if (LocToVal.size() != JoinedEnv.LocToVal.size())
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
@@ -179,7 +179,9 @@
   Context.addFlowConditionConstraint(FC2, C2);
   Context.addFlowConditionConstraint(FC2, C3);
 
-  auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+  auto &B1 = Context.createAtomicBoolValue();
+  auto &B2 = Context.createAtomicBoolValue();
+  auto &FC3 = Context.joinFlowConditions(FC1, FC2, B1, B2);
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
   EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
   EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
@@ -436,7 +438,9 @@
   auto &FC2 = Context.makeFlowConditionToken();
   Context.addFlowConditionConstraint(FC2, Y);
   // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
-  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
+  auto &B1 = Context.createAtomicBoolValue();
+  auto &B2 = Context.createAtomicBoolValue();
+  auto &JoinedFC = Context.joinFlowConditions(FC1, FC2, B1, B2);
   Context.addFlowConditionConstraint(JoinedFC, Z);
 
   // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent