diff --git a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
index d397e47224..216fb3d4b0 100644
--- a/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -285,8 +285,8 @@ namespace {
 class RangeConstraintManager : public SimpleConstraintManager{
   RangeSet GetRange(ProgramStateRef state, SymbolRef sym);
 public:
-  RangeConstraintManager(SubEngine *subengine, BasicValueFactory &BVF)
-    : SimpleConstraintManager(subengine, BVF) {}
+  RangeConstraintManager(SubEngine *subengine, SValBuilder &SVB)
+    : SimpleConstraintManager(subengine, SVB) {}
 
   ProgramStateRef assumeSymNE(ProgramStateRef state, SymbolRef sym,
                              const llvm::APSInt& Int,
@@ -328,7 +328,7 @@ private:
 
 ConstraintManager *
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
-  return new RangeConstraintManager(Eng, StMgr.getBasicVals());
+  return new RangeConstraintManager(Eng, StMgr.getSValBuilder());
 }
 
 const llvm::APSInt* RangeConstraintManager::getSymVal(ProgramStateRef St,
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
index de13241cac..86940a1e84 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
@@ -49,6 +49,11 @@ bool SimpleConstraintManager::canReasonAbout(SVal X) const {
       }
     }
 
+    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
+      if (SSE->getOpcode() == BO_EQ || SSE->getOpcode() == BO_NE)
+        return true;
+    }
+
     return false;
   }
 
@@ -164,8 +169,6 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
     return assumeAuxForSymbol(state, sym, Assumption);
   }
 
-  BasicValueFactory &BasicVals = getBasicVals();
-
   switch (Cond.getSubKind()) {
   default:
     llvm_unreachable("'Assume' not implemented for this NonLoc");
@@ -180,26 +183,43 @@ ProgramStateRef SimpleConstraintManager::assumeAux(ProgramStateRef state,
       return assumeAuxForSymbol(state, sym, Assumption);
 
     // Handle symbolic expression.
-    } else {
+    } else if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym)) {
       // We can only simplify expressions whose RHS is an integer.
-      const SymIntExpr *SE = dyn_cast<SymIntExpr>(sym);
-      if (!SE)
-        return assumeAuxForSymbol(state, sym, Assumption);
 
       BinaryOperator::Opcode op = SE->getOpcode();
-      // Implicitly compare non-comparison expressions to 0.
-      if (!BinaryOperator::isComparisonOp(op)) {
-        QualType T = SE->getType();
-        const llvm::APSInt &zero = BasicVals.getValue(0, T);
-        op = (Assumption ? BO_NE : BO_EQ);
-        return assumeSymRel(state, SE, op, zero);
-      }
-      // From here on out, op is the real comparison we'll be testing.
-      if (!Assumption)
-        op = NegateComparison(op);
+      if (BinaryOperator::isComparisonOp(op)) {
+        if (!Assumption)
+          op = NegateComparison(op);
 
-      return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
+        return assumeSymRel(state, SE->getLHS(), op, SE->getRHS());
+      }
+
+    } else if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(sym)) {
+      BinaryOperator::Opcode Op = SSE->getOpcode();
+
+      // Translate "a != b" to "(b - a) != 0".
+      // We invert the order of the operands as a heuristic for how loop
+      // conditions are usually written ("begin != end") as compared to length
+      // calculations ("end - begin"). The more correct thing to do would be to
+      // canonicalize "a - b" and "b - a", which would allow us to treat
+      // "a != b" and "b != a" the same.
+      if (BinaryOperator::isEqualityOp(Op)) {
+        SymbolManager &SymMgr = getSymbolManager();
+
+        assert(Loc::isLocType(SSE->getLHS()->getType()));
+        assert(Loc::isLocType(SSE->getRHS()->getType()));
+        QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+        SymbolRef Subtraction = SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub,
+                                                     SSE->getLHS(), DiffTy);
+
+        Assumption ^= (SSE->getOpcode() == BO_EQ);
+        return assumeAuxForSymbol(state, Subtraction, Assumption);
+      }
     }
+
+    // If we get here, there's nothing else we can do but treat the symbol as
+    // opaque.
+    return assumeAuxForSymbol(state, sym, Assumption);
   }
 
   case nonloc::ConcreteIntKind: {
diff --git a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
index 01f0b4e446..10ddef1341 100644
--- a/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
+++ b/lib/StaticAnalyzer/Core/SimpleConstraintManager.h
@@ -23,10 +23,10 @@ namespace ento {
 
 class SimpleConstraintManager : public ConstraintManager {
   SubEngine *SU;
-  BasicValueFactory &BVF;
+  SValBuilder &SVB;
 public:
-  SimpleConstraintManager(SubEngine *subengine, BasicValueFactory &BV)
-    : SU(subengine), BVF(BV) {}
+  SimpleConstraintManager(SubEngine *subengine, SValBuilder &SB)
+    : SU(subengine), SVB(SB) {}
   virtual ~SimpleConstraintManager();
 
   //===------------------------------------------------------------------===//
@@ -81,7 +81,8 @@ protected:
   // Internal implementation.
   //===------------------------------------------------------------------===//
 
-  BasicValueFactory &getBasicVals() const { return BVF; }
+  BasicValueFactory &getBasicVals() const { return SVB.getBasicValueFactory(); }
+  SymbolManager &getSymbolManager() const { return SVB.getSymbolManager(); }
 
   bool canReasonAbout(SVal X) const;
 
diff --git a/test/Analysis/ptr-arith.c b/test/Analysis/ptr-arith.c
index 7f2582dc24..d9c5a0ff99 100644
--- a/test/Analysis/ptr-arith.c
+++ b/test/Analysis/ptr-arith.c
@@ -179,3 +179,60 @@ void use_symbols(int *lhs, int *rhs) {
     return;
   clang_analyzer_eval((lhs - rhs) == 5); // expected-warning{{TRUE}}
 }
+
+void equal_implies_zero(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
+  if (lhs == rhs) {
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{TRUE}}
+    return;
+  }
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+  clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+  clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+}
+
+void zero_implies_equal(int *lhs, int *rhs) {
+  clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
+  if ((rhs - lhs) == 0) {
+    clang_analyzer_eval(lhs != rhs); // expected-warning{{FALSE}}
+    clang_analyzer_eval(lhs == rhs); // expected-warning{{TRUE}}
+    return;
+  }
+  clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+  clang_analyzer_eval(lhs != rhs); // expected-warning{{TRUE}}
+}
+
+//-------------------------------
+// False positives
+//-------------------------------
+
+void zero_implies_reversed_equal(int *lhs, int *rhs) {
+  clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{UNKNOWN}}
+  if ((rhs - lhs) == 0) {
+    // FIXME: Should be FALSE.
+    clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
+    // FIXME: Should be TRUE.
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+    return;
+  }
+  clang_analyzer_eval((rhs - lhs) == 0); // expected-warning{{FALSE}}
+  // FIXME: Should be FALSE.
+  clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+  // FIXME: Should be TRUE.
+  clang_analyzer_eval(rhs != lhs); // expected-warning{{UNKNOWN}}
+}
+
+void canonical_equal(int *lhs, int *rhs) {
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{UNKNOWN}}
+  if (lhs == rhs) {
+    // FIXME: Should be TRUE.
+    clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+    return;
+  }
+  clang_analyzer_eval(lhs == rhs); // expected-warning{{FALSE}}
+
+  // FIXME: Should be FALSE.
+  clang_analyzer_eval(rhs == lhs); // expected-warning{{UNKNOWN}}
+}