Index: include/clang/AST/Expr.h
===================================================================
--- include/clang/AST/Expr.h
+++ include/clang/AST/Expr.h
@@ -875,7 +875,7 @@
     : Expr(OpaqueValueExprClass, T, VK, OK,
            T->isDependentType() ||
            (SourceExpr && SourceExpr->isTypeDependent()),
-           T->isDependentType() || 
+           T->isDependentType() ||
            (SourceExpr && SourceExpr->isValueDependent()),
            T->isInstantiationDependentType() ||
            (SourceExpr && SourceExpr->isInstantiationDependent()),
@@ -3103,6 +3103,13 @@
   }
   bool isAssignmentOp() const { return isAssignmentOp(getOpcode()); }
 
+  static bool isCommutativeOp(Opcode Opc) {
+    return Opc == BO_Mul || Opc == BO_Add || (Opc >= BO_EQ && Opc <= BO_Or);
+  }
+  bool isCommutativeOp() const {
+    return isCommutativeOp(getOpcode());
+  }
+
   static bool isCompoundAssignmentOp(Opcode Opc) {
     return Opc > BO_Assign && Opc <= BO_OrAssign;
   }
@@ -5229,7 +5236,7 @@
 
   SourceLocation getLocStart() const LLVM_READONLY { return SourceLocation(); }
   SourceLocation getLocEnd() const LLVM_READONLY { return SourceLocation(); }
-  
+
   static bool classof(const Stmt *T) {
     return T->getStmtClass() == TypoExprClass;
   }
Index: include/clang/Config/config.h.cmake
===================================================================
--- include/clang/Config/config.h.cmake
+++ include/clang/Config/config.h.cmake
@@ -38,7 +38,7 @@
 /* Define if we have libxml2 */
 #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
 
-/* Define if we have z3 and want to build it */
+/* Define if we have z3 and want to build with it */
 #cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
 
 /* Define if we have sys/resource.h (rlimits) */
Index: include/clang/StaticAnalyzer/Checkers/SValExplainer.h
===================================================================
--- include/clang/StaticAnalyzer/Checkers/SValExplainer.h
+++ include/clang/StaticAnalyzer/Checkers/SValExplainer.h
@@ -125,8 +125,14 @@
     return OS.str();
   }
 
-  // TODO: IntSymExpr doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitIntSymExpr(const IntSymExpr *S) {
+    std::string Str;
+    llvm::raw_string_ostream OS(Str);
+    OS << S->getLHS()
+       << std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) << " "
+       << "(" << Visit(S->getRHS()) << ") ";
+    return OS.str();
+  }
 
   std::string VisitSymSymExpr(const SymSymExpr *S) {
     return "(" + Visit(S->getLHS()) + ") " +
@@ -134,8 +140,10 @@
            " (" + Visit(S->getRHS()) + ")";
   }
 
-  // TODO: SymbolCast doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitSymbolCast(const SymbolCast *S) {
+    return "cast of type '" + S->getType().getAsString() + "' of " +
+           Visit(S->getOperand());
+  }
 
   std::string VisitSymbolicRegion(const SymbolicRegion *R) {
     // Explain 'this' object here.
Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -263,6 +263,12 @@
   /// \sa getGraphTrimInterval
   Optional<unsigned> GraphTrimInterval;
 
+  /// \sa getMaxSimplifyComplexity
+  Optional<unsigned> MaxSimplifyComplexity;
+
+  /// \sa getMaxTaintComplexity
+  Optional<unsigned> MaxTaintComplexity;
+
   /// \sa getMaxTimesInlineLarge
   Optional<unsigned> MaxTimesInlineLarge;
 
@@ -546,6 +552,18 @@
   /// node reclamation, set the option to "0".
   unsigned getGraphTrimInterval();
 
+  /// Returns the maximum complexity of symbolic constraint to generate
+  /// when taint analysis checkers are enabled (10000 by default).
+  ///
+  /// This is controlled by "-analyzer-config max-simplify-complexity" option.
+  unsigned getMaxSimplifyComplexity();
+
+  /// Returns the maximum complexity of symbolic constraints to simplify
+  /// through recursive evaluation (10 by default).
+  ///
+  /// This is controlled by "-analyzer-config max-taint-complexity" option.
+  unsigned getMaxTaintComplexity();
+
   /// Returns the maximum times a large function could be inlined.
   ///
   /// This is controlled by the 'max-times-inline-large' config option.
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -85,7 +85,7 @@
       // does not. Is there a good equivalent there?
       assert(assume(State, Cond, false) && "System is over constrained.");
 #endif
-      return ProgramStatePair((ProgramStateRef)nullptr, State);
+      return ProgramStatePair((ProgramStateRef) nullptr, State);
     }
 
     ProgramStateRef StFalse = assume(State, Cond, false);
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -324,6 +324,18 @@
   return GraphTrimInterval.getValue();
 }
 
+unsigned AnalyzerOptions::getMaxSimplifyComplexity() {
+  if (!MaxSimplifyComplexity.hasValue())
+    MaxSimplifyComplexity = getOptionAsInteger("max-simplify-complexity", 10);
+  return MaxSimplifyComplexity.getValue();
+}
+
+unsigned AnalyzerOptions::getMaxTaintComplexity() {
+  if (!MaxTaintComplexity.hasValue())
+    MaxTaintComplexity = getOptionAsInteger("max-taint-complexity", 10000);
+  return MaxTaintComplexity.getValue();
+}
+
 unsigned AnalyzerOptions::getMaxTimesInlineLarge() {
   if (!MaxTimesInlineLarge.hasValue())
     MaxTimesInlineLarge = getOptionAsInteger("max-times-inline-large", 32);
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -370,42 +370,57 @@
 
 bool RangeConstraintManager::canReasonAbout(SVal X) const {
   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-  if (SymVal && SymVal->isExpression()) {
-    const SymExpr *SE = SymVal->getSymbol();
-
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
-      switch (SIE->getOpcode()) {
-      // We don't reason yet about bitwise-constraints on symbolic values.
-      case BO_And:
-      case BO_Or:
-      case BO_Xor:
-        return false;
-      // We don't reason yet about these arithmetic constraints on
-      // symbolic values.
-      case BO_Mul:
-      case BO_Div:
-      case BO_Rem:
-      case BO_Shl:
-      case BO_Shr:
+  if (!SymVal)
+    return true;
+
+  const SymExpr *SE = SymVal->getSymbol();
+  do {
+    if (isa<SymbolData>(SE)) {
+      return true;
+    }
+
+    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(SE)) {
+      BinaryOperator::Opcode Op = BSE->getOpcode();
+
+      if (isa<IntSymExpr>(BSE)) {
         return false;
-      // All other cases.
-      default:
+      }
+
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+        if (BinaryOperator::isMultiplicativeOp(Op) ||
+            BinaryOperator::isShiftOp(Op) || BinaryOperator::isBitwiseOp(Op)) {
+          // We don't reason yet about bitwise-constraints on symbolic values.
+          // We don't reason yet about arithmetic constraints on symbolic values
+          return false;
+        }
+
+        // The simplification case of RangedConstraintManager::assumeSymRel()
+        if (isa<BinarySymExpr>(SIE->getLHS()) &&
+            BinaryOperator::isEqualityOp(Op) && SIE->getRHS() == 0 &&
+            BinaryOperator::isComparisonOp(
+                cast<BinarySymExpr>(SIE->getLHS())->getOpcode())) {
+          SE = SIE->getLHS();
+          continue;
+        }
+
         return true;
       }
-    }
 
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
+      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE)) {
+        if (!BinaryOperator::isComparisonOp(Op) ||
+            !Loc::isLocType(SSE->getLHS()->getType()) ||
+            !Loc::isLocType(SSE->getRHS()->getType())) {
+          // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+          return false;
         }
+
+        return canReasonAbout(nonloc::SymbolVal(SSE->getLHS())) &&
+               canReasonAbout(nonloc::SymbolVal(SSE->getRHS()));
       }
     }
 
     return false;
-  }
+  } while (SE);
 
   return true;
 }
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -130,8 +130,9 @@
   // "exp comparison_op expr" to false.)
   if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
     if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
-      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+      if (BinaryOperator::isComparisonOp(SE->getOpcode())) {
         return assumeSym(State, Sym, (Op == BO_NE ? true : false));
+      }
   }
 
   // Get the type used for calculating wraparound.
Index: lib/StaticAnalyzer/Core/SValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SValBuilder.cpp
@@ -15,10 +15,13 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/AST/DeclCXX.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 
 using namespace clang;
 using namespace ento;
@@ -100,7 +103,7 @@
 
   if (T->isNullPtrType())
     return makeZeroVal(T);
-  
+
   if (!SymbolManager::canSymbolicate(T))
     return UnknownVal();
 
@@ -354,17 +357,17 @@
                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
-
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
   // TODO: When the Max Complexity is reached, we should conjure a symbol
   // instead of generating an Unknown value and propagate the taint info to it.
-  const unsigned MaxComp = 10000; // 100000 28X
+
+  AnalyzerOptions &Opts =
+      StateMgr.getOwningEngine()->getAnalysisManager().options;
+  const unsigned MaxComp = Opts.getMaxTaintComplexity(); // 100000 28X
 
   if (symLHS && symRHS &&
-      (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+      (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
     return makeNonLoc(symLHS, Op, symRHS, ResultTy);
 
   if (symLHS && symLHS->computeComplexity() < MaxComp)
@@ -378,7 +381,6 @@
   return UnknownVal();
 }
 
-
 SVal SValBuilder::evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
                             SVal lhs, SVal rhs, QualType type) {
 
Index: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
===================================================================
--- lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
+++ lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
@@ -12,9 +12,12 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 
 using namespace clang;
 using namespace ento;
@@ -677,14 +680,18 @@
     // If one of the operands is a symbol and the other is a constant,
     // build an expression for use by the constraint manager.
     if (SymbolRef rSym = rhs.getAsLocSymbol()) {
-      // We can only build expressions with symbols on the left,
-      // so we need a reversible operator.
-      if (!BinaryOperator::isComparisonOp(op))
-        return UnknownVal();
-
       const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
-      op = BinaryOperator::reverseComparisonOp(op);
-      return makeNonLoc(rSym, op, lVal, resultTy);
+
+      if (BinaryOperator::isCommutativeOp(op))
+        return makeNonLoc(rSym, op, lVal, resultTy);
+
+      if (BinaryOperator::isComparisonOp(op)) {
+        BinaryOperator::Opcode NewOp = BinaryOperator::reverseComparisonOp(op);
+        return makeNonLoc(rSym, NewOp, lVal, resultTy);
+      }
+
+      // Prefer expressions with symbols on the left
+      return makeNonLoc(lVal, op, rSym, resultTy);
     }
 
     // If both operands are constants, just perform the operation.
@@ -1002,7 +1009,8 @@
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs.
+  // FIXME: Add support for SymExprs in RangeConstraintManager.
+
   return nullptr;
 }
 
@@ -1014,22 +1022,30 @@
   class Simplifier : public FullSValVisitor<Simplifier, SVal> {
     ProgramStateRef State;
     SValBuilder &SVB;
+    AnalyzerOptions &Opts;
 
   public:
     Simplifier(ProgramStateRef State)
-        : State(State), SVB(State->getStateManager().getSValBuilder()) {}
+        : State(State), SVB(State->getStateManager().getSValBuilder()),
+          Opts(State->getStateManager()
+                   .getOwningEngine()
+                   ->getAnalysisManager()
+                   .options) {}
 
     SVal VisitSymbolData(const SymbolData *S) {
       if (const llvm::APSInt *I =
               SVB.getKnownValue(State, nonloc::SymbolVal(S)))
         return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
                                             : (SVal)SVB.makeIntVal(*I);
-      return Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S) 
+      return Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S)
                                           : nonloc::SymbolVal(S);
     }
 
-    // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
-    // start producing them.
+    SVal VisitIntSymExpr(const IntSymExpr *S) {
+      SVal RHS = Visit(S->getRHS());
+      SVal LHS = SVB.makeIntVal(S->getLHS());
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
 
     SVal VisitSymIntExpr(const SymIntExpr *S) {
       SVal LHS = Visit(S->getLHS());
@@ -1054,6 +1070,11 @@
       return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
     }
 
+    SVal VisitSymbolCast(const SymbolCast *S) {
+      SVal V = Visit(S->getOperand());
+      return SVB.evalCast(V, S->getType(), S->getOperand()->getType());
+    }
+
     SVal VisitSymSymExpr(const SymSymExpr *S) {
       SVal LHS = Visit(S->getLHS());
       SVal RHS = Visit(S->getRHS());
@@ -1067,7 +1088,11 @@
     SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
       // Simplification is much more costly than computing complexity.
       // For high complexity, it may be not worth it.
-      if (V.getSymbol()->computeComplexity() > 100)
+      // Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
+
+      // FIXME: Complexity monotonically decreases in child recursive calls,
+      // avoid calling this repeatedly
+      if (V.getSymbol()->computeComplexity() > Opts.getMaxSimplifyComplexity())
         return V;
       return Visit(V.getSymbol());
     }
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -987,6 +987,10 @@
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt &Int) const;
 
+  // Fix the input APSInt if it is has a bitwidth of 1, and set the type.
+  const llvm::APSInt &fixAPSInt(const llvm::APSInt &Int, llvm::APSInt &NewInt,
+                                QualType *Ty = nullptr) const;
+
   // Perform implicit type conversion on binary symbolic expressions.
   // May modify all input parameters.
   // TODO: Refactor to use built-in conversion functions
@@ -1037,28 +1041,29 @@
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
   Z3Expr Exp = getZ3Expr(Sym, &RetTy);
-
-  assert((getAPSIntType(From) == getAPSIntType(To)) &&
-         "Range values have different types!");
-  QualType RTy = getAPSIntType(From);
-  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
-  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
-  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+  QualType LTy;
+  llvm::APSInt NewFromInt;
+  Z3Expr FromExp = Z3Expr::fromAPSInt(fixAPSInt(From, NewFromInt, &LTy));
 
   // Construct single (in)equality
   if (From == To)
     return assumeZ3Expr(State, Sym,
                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
-                                     FromExp, RTy, nullptr));
+                                     FromExp, LTy, nullptr));
 
+  QualType RTy;
+  llvm::APSInt NewToInt;
+  Z3Expr ToExp = Z3Expr::fromAPSInt(fixAPSInt(To, NewToInt, &RTy));
+  assert(LTy == RTy && "Range values have different types!");
   // Construct two (in)equalities, and a logical and/or
   Z3Expr LHS =
-      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, LTy, nullptr);
   Z3Expr RHS =
       getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
   return assumeZ3Expr(
       State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                        RetTy->isSignedIntegerOrEnumerationType()));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
@@ -1145,8 +1150,8 @@
 
 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
                                                    SymbolRef Sym) const {
-  BasicValueFactory &BV = getBasicVals();
-  ASTContext &Ctx = BV.getContext();
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
 
   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
     QualType Ty = Sym->getType();
@@ -1180,7 +1185,7 @@
       return nullptr;
 
     // This is the only solution, store it
-    return &BV.getValue(Value);
+    return &BVF.getValue(Value);
   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
     SymbolRef CastSym = SC->getOperand();
     QualType CastTy = SC->getType();
@@ -1191,7 +1196,7 @@
     const llvm::APSInt *Value;
     if (!(Value = getSymVal(State, CastSym)))
       return nullptr;
-    return &BV.Convert(SC->getType(), *Value);
+    return &BVF.Convert(SC->getType(), *Value);
   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
     const llvm::APSInt *LHS, *RHS;
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
@@ -1215,7 +1220,7 @@
     QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
     doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
         ConvertedLHS, LTy, ConvertedRHS, RTy);
-    return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
   }
 
   llvm_unreachable("Unsupported expression to get symbol value!");
@@ -1342,13 +1347,13 @@
   BinaryOperator::Opcode Op = BSE->getOpcode();
 
   if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-    RTy = getAPSIntType(SIE->getRHS());
+    llvm::APSInt NewRInt;
     Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
-    Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+    Z3Expr RHS = Z3Expr::fromAPSInt(fixAPSInt(SIE->getRHS(), NewRInt, &RTy));
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-    LTy = getAPSIntType(ISE->getLHS());
-    Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+    llvm::APSInt NewLInt;
+    Z3Expr LHS = Z3Expr::fromAPSInt(fixAPSInt(ISE->getLHS(), NewLInt, &LTy));
     Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
@@ -1402,10 +1407,30 @@
   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
 }
 
+const llvm::APSInt &Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int,
+                                                   llvm::APSInt &NewInt,
+                                                   QualType *Ty) const {
+  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+  // but the former is not available in Clang. Instead, extend the APSInt
+  // directly.
+  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+    ASTContext &Ctx = getBasicVals().getContext();
+    NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+    if (Ty)
+      *Ty = getAPSIntType(NewInt);
+    return NewInt;
+  }
+
+  if (Ty)
+    *Ty = getAPSIntType(Int);
+  return Int;
+}
+
 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
                                            QualType &LTy, QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
       RTy->isIntegralOrEnumerationType()) {
@@ -1468,10 +1493,10 @@
 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
                                               QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
-
   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Always perform integer promotion before checking type equality.
   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
   if (LTy->isPromotableIntegerType()) {
@@ -1612,7 +1637,9 @@
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
-  llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
+                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           false);
   return nullptr;
 #endif
 }
Index: test/Analysis/analyzer_test.py
===================================================================
--- test/Analysis/analyzer_test.py
+++ test/Analysis/analyzer_test.py
@@ -1,3 +1,4 @@
+import copy
 import lit.formats
 import lit.TestRunner
 
@@ -8,18 +9,21 @@
         results = []
 
         # Parse any test requirements ('REQUIRES: ')
-        saved_test = test
+        saved_test = copy.deepcopy(test)
         lit.TestRunner.parseIntegratedTestScript(test)
 
+        # If the test does not require z3, drop it from the available features
+        # to satisfy tests that explicitly require !z3
         if 'z3' not in test.requires:
+            test.config.available_features.discard('z3')
             results.append(self.executeWithAnalyzeSubstitution(
-                saved_test, litConfig, '-analyzer-constraints=range'))
+                test, litConfig, '-analyzer-constraints=range'))
 
-            if results[-1].code == lit.Test.FAIL:
+            if results[-1].code != lit.Test.PASS:
                 return results[-1]
 
         # If z3 backend available, add an additional run line for it
-        if test.config.clang_staticanalyzer_z3 == '1':
+        if test.config.clang_staticanalyzer_z3 == '1' and '!z3' not in test.requires:
             results.append(self.executeWithAnalyzeSubstitution(
                 saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
 
Index: test/Analysis/bitwise-ops.c
===================================================================
--- test/Analysis/bitwise-ops.c
+++ test/Analysis/bitwise-ops.c
@@ -7,10 +7,9 @@
   // Sanity check
   CHECK(x); // expected-warning{{TRUE}}
   CHECK(x & 1); // expected-warning{{TRUE}}
-  
-  // False positives due to SValBuilder giving up on certain kinds of exprs.
-  CHECK(1 - x); // expected-warning{{UNKNOWN}}
-  CHECK(x & y); // expected-warning{{UNKNOWN}}
+
+  CHECK(1 - x); // expected-warning{{TRUE}}
+  CHECK(x & y); // expected-warning{{TRUE}}
 }
 
 int testConstantShifts_PR18073(int which) {
@@ -29,4 +28,4 @@
   default:
     return 0;
   }
-}
\ No newline at end of file
+}
Index: test/Analysis/bool-assignment.c
===================================================================
--- test/Analysis/bool-assignment.c
+++ test/Analysis/bool-assignment.c
@@ -43,15 +43,11 @@
     return;
   }
   if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
     BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
-    BOOL x = y; // no-warning
-#endif
     return;
   }
   if (y >= 127 && y < 150) {
-    BOOL x = y; // expected-warning{{Assignment of a non-Boolean value}}
+    BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
     return;
   }
   if (y > 1) {
Index: test/Analysis/conditional-path-notes.c
===================================================================
--- test/Analysis/conditional-path-notes.c
+++ test/Analysis/conditional-path-notes.c
@@ -77,7 +77,8 @@
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-    // expected-note@-1 {{Taking true branch}}
+    // expected-note@-1 {{Assuming the condition is true}}
+    // expected-note@-2 {{Taking true branch}}
     *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
     // expected-note@-1 {{Dereference of null pointer}}
   }
@@ -1573,12 +1574,75 @@
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>79</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>11</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1594,12 +1658,12 @@
 // CHECK-NEXT:         <key>start</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1607,12 +1671,12 @@
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
@@ -1624,7 +1688,7 @@
 // CHECK-NEXT:      <key>kind</key><string>event</string>
 // CHECK-NEXT:      <key>location</key>
 // CHECK-NEXT:      <dict>
-// CHECK-NEXT:       <key>line</key><integer>81</integer>
+// CHECK-NEXT:       <key>line</key><integer>82</integer>
 // CHECK-NEXT:       <key>col</key><integer>24</integer>
 // CHECK-NEXT:       <key>file</key><integer>0</integer>
 // CHECK-NEXT:      </dict>
@@ -1632,12 +1696,12 @@
 // CHECK-NEXT:      <array>
 // CHECK-NEXT:        <array>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>5</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>26</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
@@ -1658,10 +1722,10 @@
 // CHECK-NEXT:    <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
 // CHECK-NEXT:   <key>issue_context_kind</key><string>function</string>
 // CHECK-NEXT:   <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
-// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>3</string>
+// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>4</string>
 // CHECK-NEXT:   <key>location</key>
 // CHECK-NEXT:   <dict>
-// CHECK-NEXT:    <key>line</key><integer>81</integer>
+// CHECK-NEXT:    <key>line</key><integer>82</integer>
 // CHECK-NEXT:    <key>col</key><integer>24</integer>
 // CHECK-NEXT:    <key>file</key><integer>0</integer>
 // CHECK-NEXT:   </dict>
Index: test/Analysis/explain-svals.cpp
===================================================================
--- test/Analysis/explain-svals.cpp
+++ test/Analysis/explain-svals.cpp
@@ -69,7 +69,7 @@
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}}
   clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}}
-  clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}}
+  clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}}
   clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}}
   clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}}
   clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}}
Index: test/Analysis/loop-unrolling.cpp
===================================================================
--- test/Analysis/loop-unrolling.cpp
+++ test/Analysis/loop-unrolling.cpp
@@ -252,7 +252,11 @@
 int nested_inlined_no_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
+#ifdef ANALYZER_CM_Z3
+    clang_analyzer_numTimesReached(); // expected-warning {{13}}
+#else
     clang_analyzer_numTimesReached(); // expected-warning {{15}}
+#endif
     k = simple_unknown_bound_loop();  // reevaluation without inlining, splits the state as well
   }
   int a = 22 / k; // no-warning
Index: test/Analysis/plist-macros-z3.cpp
===================================================================
--- test/Analysis/plist-macros-z3.cpp
+++ test/Analysis/plist-macros-z3.cpp
@@ -1,7 +1,7 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
-
+// REQUIRES: z3
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
@@ -11,13 +11,13 @@
   y++;
   y--;
   mallocmemory
-  y++; 
+  y++;
   y++;
   delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
 }
 
 void macroIsFirstInFunction(int y) {
-  mallocmemory 
+  mallocmemory
   y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
 }
 
@@ -39,7 +39,7 @@
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
-#define macroWithArg(mp) mp==0 
+#define macroWithArg(mp) mp==0
 int macroWithArgInExpression(int *p, int y) {;
   y++;
   if (macroWithArg(p))
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  <key>diagnostics</key>
 // CHECK-NEXT:  <array>
 // CHECK-NEXT:   <dict>
Index: test/Analysis/plist-macros.cpp
===================================================================
--- test/Analysis/plist-macros.cpp
+++ test/Analysis/plist-macros.cpp
@@ -1,7 +1,7 @@
 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
-
+// REQUIRES: !z3
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
@@ -11,13 +11,13 @@
   y++;
   y--;
   mallocmemory
-  y++; 
+  y++;
   y++;
   delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
 }
 
 void macroIsFirstInFunction(int y) {
-  mallocmemory 
+  mallocmemory
   y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
 }
 
@@ -39,7 +39,7 @@
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
-#define macroWithArg(mp) mp==0 
+#define macroWithArg(mp) mp==0
 int macroWithArgInExpression(int *p, int y) {;
   y++;
   if (macroWithArg(p))
@@ -85,6 +85,7 @@
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  <key>diagnostics</key>
 // CHECK-NEXT:  <array>
 // CHECK-NEXT:   <dict>
@@ -636,6 +637,69 @@
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>36</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>25</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
 // CHECK-NEXT:            <key>line</key><integer>37</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
Index: test/Analysis/range_casts.c
===================================================================
--- test/Analysis/range_casts.c
+++ test/Analysis/range_casts.c
@@ -67,7 +67,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
+  if (index - 1 == 0)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -87,7 +87,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
+  if (index - 1L == 0L)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
@@ -117,7 +117,7 @@
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
+  if (index - 1UL == 0L)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
Index: test/Analysis/std-c-library-functions.c
===================================================================
--- test/Analysis/std-c-library-functions.c
+++ test/Analysis/std-c-library-functions.c
@@ -57,8 +57,7 @@
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);