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
@@ -263,30 +263,51 @@
       const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
       const Variable RightSubVar = GetVar(&C->getRightSubValue());
 
-      // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
-      // which is already in conjunctive normal form. Below we add each of the
-      // conjuncts of the latter expression to the result.
-      Formula.addClause(negLit(Var), posLit(LeftSubVar));
-      Formula.addClause(negLit(Var), posLit(RightSubVar));
-      Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&C->getLeftSubValue());
-      UnprocessedSubVals.push(&C->getRightSubValue());
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
+        // already in conjunctive normal form. Below we add each of the
+        // conjuncts of the latter expression to the result.
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+
+        // Visit a sub-value of `Val` (pick any, they are identical).
+      } else {
+        // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
+        // which is already in conjunctive normal form. Below we add each of the
+        // conjuncts of the latter expression to the result.
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(negLit(Var), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&C->getLeftSubValue());
+        UnprocessedSubVals.push(&C->getRightSubValue());
+      }
     } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
       const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
       const Variable RightSubVar = GetVar(&D->getRightSubValue());
 
-      // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
-      // which is already in conjunctive normal form. Below we add each of the
-      // conjuncts of the latter expression to the result.
-      Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
-      Formula.addClause(posLit(Var), negLit(LeftSubVar));
-      Formula.addClause(posLit(Var), negLit(RightSubVar));
+      if (LeftSubVar == RightSubVar) {
+        // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
+        // already in conjunctive normal form. Below we add each of the
+        // conjuncts of the latter expression to the result.
+        Formula.addClause(negLit(Var), posLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
 
-      // Visit the sub-values of `Val`.
-      UnprocessedSubVals.push(&D->getLeftSubValue());
-      UnprocessedSubVals.push(&D->getRightSubValue());
+        // Visit a sub-value of `Val` (pick any, they are identical).
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+      } else {
+        // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
+        // which is already in conjunctive normal form. Below we add each of the
+        // conjuncts of the latter expression to the result.
+        Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
+        Formula.addClause(posLit(Var), negLit(LeftSubVar));
+        Formula.addClause(posLit(Var), negLit(RightSubVar));
+
+        // Visit the sub-values of `Val`.
+        UnprocessedSubVals.push(&D->getLeftSubValue());
+        UnprocessedSubVals.push(&D->getRightSubValue());
+      }
     } else if (auto *N = dyn_cast<NegationValue>(Val)) {
       const Variable SubVar = GetVar(&N->getSubVal());
 
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
@@ -120,7 +120,7 @@
   expectUnsatisfiable(solve({NotXAndY, XAndY}));
 }
 
-TEST(SolverTest, DisjunctionSameVars) {
+TEST(SolverTest, DisjunctionSameVarWithNegation) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
   auto NotX = Ctx.neg(X);
@@ -130,6 +130,15 @@
   expectSatisfiable(solve({XOrNotX}), _);
 }
 
+TEST(SolverTest, DisjunctionSameVar) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto XOrX = Ctx.disj(X, X);
+
+  // X v X
+  expectSatisfiable(solve({XOrX}), _);
+}
+
 TEST(SolverTest, ConjunctionSameVarsConflict) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();
@@ -140,6 +149,15 @@
   expectUnsatisfiable(solve({XAndNotX}));
 }
 
+TEST(SolverTest, ConjunctionSameVar) {
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto XAndX = Ctx.conj(X, X);
+
+  // X ^ X
+  expectSatisfiable(solve({XAndX}), _);
+}
+
 TEST(SolverTest, PureVar) {
   ConstraintContext Ctx;
   auto X = Ctx.atom();