diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -256,7 +256,7 @@
   ///  by FoldingSet.
   void Profile(llvm::FoldingSetNodeID &ID) const { Profile(ID, *this); }
 
-  /// getConcreteValue - If a symbol is contrained to equal a specific integer
+  /// getConcreteValue - If a symbol is constrained to equal a specific integer
   ///  constant then this method returns that value.  Otherwise, it returns
   ///  NULL.
   const llvm::APSInt *getConcreteValue() const {
diff --git a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
--- a/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -20,6 +20,7 @@
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/SmallSet.h"
 #include "llvm/Support/Compiler.h"
 #include "llvm/Support/raw_ostream.h"
 #include <algorithm>
@@ -1550,9 +1551,81 @@
     return State->set<ConstraintRange>(Constraints);
   }
 
+  // Iterate over all symbols in an equivalence class and try to simplify them.
+  // Once a symbol is simplified then we check if we can merge the simplified
+  // symbol's equivalence class to the original class. This way, we simplify the
+  // classes as well: we strive to keep the number of the classes to be the
+  // absolute minimum.
+  LLVM_NODISCARD ProgramStateRef simplifyEquivalenceClass(
+      ProgramStateRef State, EquivalenceClass Class, SymbolSet ClassMembers) {
+    SValBuilder &SVB = getSValBuilder();
+    for (const SymbolRef &MemberSym : ClassMembers) {
+      SVal SimplifiedMemberVal =
+          SVB.simplifySVal(State, SVB.makeSymbolVal(MemberSym));
+      SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();
+      if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
+        ClassSet DisequalClasses = Class.getDisequalClasses(State);
+        EquivalenceClass ClassOfSimplifiedSym =
+            EquivalenceClass::find(State, SimplifiedMemberSym);
+        // We are about to add the newly simplified symbol to the existing
+        // equivalence class, but they are known to be non-equal. This is a
+        // contradiction.
+        if (DisequalClasses.contains(ClassOfSimplifiedSym))
+          return nullptr;
+        // The simplified symbol should be the member of the original Class,
+        // however, it might be in another existing Class at the moment. We
+        // have to merge these classes.
+        State = Class.merge(getBasicVals(), F, State, ClassOfSimplifiedSym);
+        if (!State)
+          return nullptr;
+      }
+    }
+    return State;
+  }
+
+  // Associate a constraint to a symbolic expression. First, we set the
+  // constraint in the State, then we try to simplify existing symbolic
+  // expressions based on the newly set constraint.
   LLVM_NODISCARD inline ProgramStateRef
   setConstraint(ProgramStateRef State, SymbolRef Sym, RangeSet Constraint) {
-    return setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+    assert(State);
+
+    State = setConstraint(State, EquivalenceClass::find(State, Sym), Constraint);
+    if (!State)
+      return nullptr;
+
+    // We have a chance to simplify existing symbolic values if the new
+    // constraint is a constant.
+    if (!Constraint.getConcreteValue())
+      return State;
+
+    llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
+    // Iterate over all equivalence classes and try to simplify them.
+    ClassMembersTy Members = State->get<ClassMembers>();
+    for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
+      EquivalenceClass Class = ClassToSymbolSet.first;
+      SymbolSet ClassMembers = ClassToSymbolSet.second;
+      State = simplifyEquivalenceClass(State, Class, ClassMembers);
+      if (!State)
+        return nullptr;
+      SimplifiedClasses.insert(Class);
+    }
+
+    // Trivial equivalence classes (those that have only one symbol member) are
+    // not stored in the State. Thus, we must skim through the constraints as
+    // well. And we try to simplify symbols in the constraints.
+    ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+    for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
+      EquivalenceClass Class = ClassConstraint.first;
+      if (SimplifiedClasses.count(Class)) // Already simplified.
+        continue;
+      SymbolSet ClassMembers = Class.getClassMembers(State);
+      State = simplifyEquivalenceClass(State, Class, ClassMembers);
+      if (!State)
+        return nullptr;
+    }
+
+    return State;
   }
 };
 
@@ -1588,6 +1661,8 @@
 
 inline EquivalenceClass EquivalenceClass::find(ProgramStateRef State,
                                                SymbolRef Sym) {
+  assert(State && "State should not be null");
+  assert(Sym && "Symbol should not be null");
   // We store far from all Symbol -> Class mappings
   if (const EquivalenceClass *NontrivialClass = State->get<ClassMap>(Sym))
     return *NontrivialClass;
diff --git a/clang/test/Analysis/find-binop-constraints.cpp b/clang/test/Analysis/find-binop-constraints.cpp
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/find-binop-constraints.cpp
@@ -0,0 +1,145 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_eval(bool);
+void clang_analyzer_warnIfReached();
+
+int test_legacy_behavior(int x, int y) {
+  if (y != 0)
+    return 0;
+  if (x + y != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
+  return y / (x + y);              // expected-warning{{Division by zero}}
+}
+
+int test_rhs_further_constrained(int x, int y) {
+  if (x + y != 0)
+    return 0;
+  if (y != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_lhs_further_constrained(int x, int y) {
+  if (x + y != 0)
+    return 0;
+  if (x != 0)
+    return 0;
+  clang_analyzer_eval(x + y == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(x == 0);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_lhs_and_rhs_further_constrained(int x, int y) {
+  if (x % y != 1)
+    return 0;
+  if (x != 1)
+    return 0;
+  if (y != 2)
+    return 0;
+  clang_analyzer_eval(x % y == 1); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 2);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_commutativity(int x, int y) {
+  if (x + y != 0)
+    return 0;
+  if (y != 0)
+    return 0;
+  clang_analyzer_eval(y + x == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y == 0);     // expected-warning{{TRUE}}
+  return 0;
+}
+
+int test_binop_when_height_is_2_r(int a, int x, int y, int z) {
+  switch (a) {
+  case 1: {
+    if (x + y + z != 0)
+      return 0;
+    if (z != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 2: {
+    if (x + y + z != 0)
+      return 0;
+    if (y != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 3: {
+    if (x + y + z != 0)
+      return 0;
+    if (x != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}}
+    break;
+  }
+  case 4: {
+    if (x + y + z != 0)
+      return 0;
+    if (x + y != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    clang_analyzer_eval(x + y == 0);     // expected-warning{{TRUE}}
+    break;
+  }
+  case 5: {
+    if (z != 0)
+      return 0;
+    if (x + y + z != 0)
+      return 0;
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    if (y != 0)
+      return 0;
+    clang_analyzer_eval(y == 0);         // expected-warning{{TRUE}}
+    clang_analyzer_eval(z == 0);         // expected-warning{{TRUE}}
+    clang_analyzer_eval(x + y + z == 0); // expected-warning{{TRUE}}
+    break;
+  }
+
+  }
+  return 0;
+}
+
+void test_equivalence_classes_are_updated(int a, int b, int c, int d) {
+  if (a + b != c)
+    return;
+  if (a != d)
+    return;
+  if (b != 0)
+    return;
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  clang_analyzer_eval(c == d); // expected-warning{{TRUE}}
+  return;
+}
+
+void test_contradiction(int a, int b, int c, int d) {
+  if (a + b != c)
+    return;
+  if (a == c)
+    return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+
+  // Bring in the contradiction.
+  if (b != 0)
+    return;
+  // Keep the symbols and the constraints! alive.
+  (void)(a * b * c * d);
+  clang_analyzer_warnIfReached(); // no-warning, i.e. UNREACHABLE
+  return;
+}