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
@@ -384,6 +384,11 @@
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
+/// Try to simplify a given symbolic expression's associated value based on the
+/// constraints in State. This is needed because the Environment bindings are
+/// not getting updated when a new constraint is added to the State.
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
+
 } // namespace ento
 } // namespace clang
 
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
@@ -1384,12 +1384,6 @@
 //                  Constraint manager implementation details
 //===----------------------------------------------------------------------===//
 
-static SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
-  SValBuilder &SVB = State->getStateManager().getSValBuilder();
-  SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
-  return SimplifiedVal.getAsSymbol();
-}
-
 class RangeConstraintManager : public RangedConstraintManager {
 public:
   RangeConstraintManager(ExprEngine *EE, SValBuilder &SVB)
@@ -1503,9 +1497,6 @@
       // This is an infeasible assumption.
       return nullptr;
 
-    if (SymbolRef SimplifiedSym = simplify(State, Sym))
-      Sym = SimplifiedSym;
-
     if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
       if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
         // If the original assumption is not Sym + Adjustment !=/</> Int,
@@ -1962,7 +1953,7 @@
     SValBuilder &SVB, RangeSet::Factory &F, ProgramStateRef State) {
   SymbolSet ClassMembers = getClassMembers(State);
   for (const SymbolRef &MemberSym : ClassMembers) {
-    SymbolRef SimplifiedMemberSym = ::simplify(State, MemberSym);
+    SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
     if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       EquivalenceClass ClassOfSimplifiedSym =
           EquivalenceClass::find(State, SimplifiedMemberSym);
@@ -2288,7 +2279,6 @@
     return St;
 
   llvm::APSInt Point = AdjustmentType.convert(Int) - Adjustment;
-
   RangeSet New = getRange(St, Sym);
   New = F.deletePoint(New, Point);
 
diff --git a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
--- a/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -23,12 +23,14 @@
 ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
                                                    SymbolRef Sym,
                                                    bool Assumption) {
+  Sym = simplify(State, Sym);
+
   // Handle SymbolData.
-  if (isa<SymbolData>(Sym)) {
+  if (isa<SymbolData>(Sym))
     return assumeSymUnsupported(State, Sym, Assumption);
 
-    // Handle symbolic expression.
-  } else if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
+  // Handle symbolic expression.
+  if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(Sym)) {
     // We can only simplify expressions whose RHS is an integer.
 
     BinaryOperator::Opcode op = SIE->getOpcode();
@@ -93,6 +95,9 @@
 ProgramStateRef RangedConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
+
+  Sym = simplify(State, Sym);
+
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
@@ -121,6 +126,8 @@
 ProgramStateRef
 RangedConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                               SymbolRef Sym, bool Assumption) {
+  Sym = simplify(State, Sym);
+
   BasicValueFactory &BVF = getBasicVals();
   QualType T = Sym->getType();
 
@@ -219,5 +226,13 @@
   }
 }
 
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
+  SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+  if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+    return SimplifiedSym;
+  return Sym;
+}
+
 } // end of namespace ento
 } // end of namespace clang
diff --git a/clang/test/Analysis/solver-sym-simplification-no-crash.c b/clang/test/Analysis/solver-sym-simplification-no-crash.c
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-no-crash.c
@@ -0,0 +1,26 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// Here, we test that symbol simplification in the solver does not produce any
+// crashes.
+
+// expected-no-diagnostics
+
+static int a, b;
+static long c;
+
+static void f(int i, int j)
+{
+    (void)(j <= 0 && i ? i : j);
+}
+
+static void g(void)
+{
+    int d = a - b | (c < 0);
+    for (;;)
+    {
+        f(d ^ c, c);
+    }
+}
diff --git a/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c b/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
new file mode 100644
--- /dev/null
+++ b/clang/test/Analysis/solver-sym-simplification-with-proper-range-type.c
@@ -0,0 +1,29 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+// Here we test that the range based solver equivalency tracking mechanism
+// assigns a properly typed range to the simplified symbol.
+
+void clang_analyzer_printState();
+void clang_analyzer_eval(int);
+
+void f(int a0, int b0, int c)
+{
+    int a1 = a0 - b0;
+    int b1 = (unsigned)a1 + c;
+    if (c == 0) {
+
+        int d = 7L / b1; // ...
+        // At this point b1 is considered non-zero, which results in a new
+        // constraint for $a0 - $b0 + $c. The type of this sym is unsigned,
+        // however, the simplified sym is $a0 - $b0 and its type is signed.
+        // This is probably the result of the inherent improper handling of
+        // casts. Anyway, Range assignment for constraints use this type
+        // information. Therefore, we must make sure that first we simplify the
+        // symbol and only then we assign the range.
+
+        clang_analyzer_eval(a0 - b0 != 0); // expected-warning{{TRUE}}
+    }
+}