diff --git a/lib/Checker/BasicConstraintManager.cpp b/lib/Checker/BasicConstraintManager.cpp
index e89546e..eee5c59 100644
--- a/lib/Checker/BasicConstraintManager.cpp
+++ b/lib/Checker/BasicConstraintManager.cpp
@@ -54,22 +54,28 @@
       ISetFactory(statemgr.getAllocator()) {}
 
   const GRState* AssumeSymNE(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AssumeSymLT(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AssumeSymGT(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AssumeSymGE(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AssumeSymLE(const GRState* state, SymbolRef sym,
-                             const llvm::APSInt& V);
+                             const llvm::APSInt& V,
+                             const llvm::APSInt& Adjustment);
 
   const GRState* AddEQ(const GRState* state, SymbolRef sym, const llvm::APSInt& V);
 
@@ -94,46 +100,52 @@
   return new BasicConstraintManager(statemgr, subengine);
 }
 
+
 const GRState*
 BasicConstraintManager::AssumeSymNE(const GRState *state, SymbolRef sym,
-                                    const llvm::APSInt& V) {
-  // First, determine if sym == X, where X != V.
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
+  // First, determine if sym == X, where X+Adjustment != V.
+  llvm::APSInt Adjusted = V-Adjustment;
   if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = (*X != V);
+    bool isFeasible = (*X != Adjusted);
     return isFeasible ? state : NULL;
   }
 
-  // Second, determine if sym != V.
-  if (isNotEqual(state, sym, V))
+  // Second, determine if sym+Adjustment != V.
+  if (isNotEqual(state, sym, Adjusted))
     return state;
 
   // If we reach here, sym is not a constant and we don't know if it is != V.
   // Make that assumption.
-  return AddNE(state, sym, V);
+  return AddNE(state, sym, Adjusted);
 }
 
-const GRState *BasicConstraintManager::AssumeSymEQ(const GRState *state,
-                                                   SymbolRef sym,
-                                                   const llvm::APSInt &V) {
-  // First, determine if sym == X, where X != V.
+const GRState*
+BasicConstraintManager::AssumeSymEQ(const GRState *state, SymbolRef sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
+  // First, determine if sym == X, where X+Adjustment != V.
+  llvm::APSInt Adjusted = V-Adjustment;
   if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = *X == V;
+    bool isFeasible = (*X == Adjusted);
     return isFeasible ? state : NULL;
   }
 
-  // Second, determine if sym != V.
-  if (isNotEqual(state, sym, V))
+  // Second, determine if sym+Adjustment != V.
+  if (isNotEqual(state, sym, Adjusted))
     return NULL;
 
   // If we reach here, sym is not a constant and we don't know if it is == V.
   // Make that assumption.
-  return AddEQ(state, sym, V);
+  return AddEQ(state, sym, Adjusted);
 }
 
-// These logic will be handled in another ConstraintManager.
-const GRState *BasicConstraintManager::AssumeSymLT(const GRState *state,
-                                                   SymbolRef sym,
-                                                   const llvm::APSInt& V) {
+// The logic for these will be handled in another ConstraintManager.
+const GRState*
+BasicConstraintManager::AssumeSymLT(const GRState *state, SymbolRef sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
   // Is 'V' the smallest possible value?
   if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
     // sym cannot be any value less than 'V'.  This path is infeasible.
@@ -141,13 +153,13 @@
   }
 
   // FIXME: For now have assuming x < y be the same as assuming sym != V;
-  return AssumeSymNE(state, sym, V);
+  return AssumeSymNE(state, sym, V, Adjustment);
 }
 
-const GRState *BasicConstraintManager::AssumeSymGT(const GRState *state,
-                                                   SymbolRef sym,
-                                                   const llvm::APSInt& V) {
-
+const GRState*
+BasicConstraintManager::AssumeSymGT(const GRState *state, SymbolRef sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
   // Is 'V' the largest possible value?
   if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
     // sym cannot be any value greater than 'V'.  This path is infeasible.
@@ -155,56 +167,60 @@
   }
 
   // FIXME: For now have assuming x > y be the same as assuming sym != V;
-  return AssumeSymNE(state, sym, V);
+  return AssumeSymNE(state, sym, V, Adjustment);
 }
 
-const GRState *BasicConstraintManager::AssumeSymGE(const GRState *state,
-                                                   SymbolRef sym,
-                                                   const llvm::APSInt &V) {
-
-  // Reject a path if the value of sym is a constant X and !(X >= V).
+const GRState*
+BasicConstraintManager::AssumeSymGE(const GRState *state, SymbolRef sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
+  // Reject a path if the value of sym is a constant X and !(X+Adj >= V).
   if (const llvm::APSInt *X = getSymVal(state, sym)) {
-    bool isFeasible = *X >= V;
+    bool isFeasible = (*X >= V-Adjustment);
     return isFeasible ? state : NULL;
   }
 
   // Sym is not a constant, but it is worth looking to see if V is the
   // maximum integer value.
   if (V == llvm::APSInt::getMaxValue(V.getBitWidth(), V.isUnsigned())) {
-    // If we know that sym != V, then this condition is infeasible since
-    // there is no other value greater than V.
-    bool isFeasible = !isNotEqual(state, sym, V);
+    llvm::APSInt Adjusted = V-Adjustment;
+
+    // If we know that sym != V (after adjustment), then this condition
+    // is infeasible since there is no other value greater than V.
+    bool isFeasible = !isNotEqual(state, sym, Adjusted);
 
     // If the path is still feasible then as a consequence we know that
-    // 'sym == V' because we cannot have 'sym > V' (no larger values).
+    // 'sym+Adjustment == V' because there are no larger values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, V) : NULL;
+    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
   }
 
   return state;
 }
 
 const GRState*
-BasicConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym,
-                                    const llvm::APSInt& V) {
-
-  // Reject a path if the value of sym is a constant X and !(X <= V).
+BasicConstraintManager::AssumeSymLE(const GRState *state, SymbolRef sym,
+                                    const llvm::APSInt &V,
+                                    const llvm::APSInt &Adjustment) {
+  // Reject a path if the value of sym is a constant X and !(X+Adj <= V).
   if (const llvm::APSInt* X = getSymVal(state, sym)) {
-    bool isFeasible = *X <= V;
+    bool isFeasible = (*X <= V-Adjustment);
     return isFeasible ? state : NULL;
   }
 
   // Sym is not a constant, but it is worth looking to see if V is the
   // minimum integer value.
   if (V == llvm::APSInt::getMinValue(V.getBitWidth(), V.isUnsigned())) {
-    // If we know that sym != V, then this condition is infeasible since
-    // there is no other value less than V.
-    bool isFeasible = !isNotEqual(state, sym, V);
+    llvm::APSInt Adjusted = V-Adjustment;
+
+    // If we know that sym != V (after adjustment), then this condition
+    // is infeasible since there is no other value less than V.
+    bool isFeasible = !isNotEqual(state, sym, Adjusted);
 
     // If the path is still feasible then as a consequence we know that
-    // 'sym == V' because we cannot have 'sym < V' (no smaller values).
+    // 'sym+Adjustment == V' because there are no smaller values.
     // Add this constraint.
-    return isFeasible ? AddEQ(state, sym, V) : NULL;
+    return isFeasible ? AddEQ(state, sym, Adjusted) : NULL;
   }
 
   return state;
@@ -213,7 +229,7 @@
 const GRState* BasicConstraintManager::AddEQ(const GRState* state, SymbolRef sym,
                                              const llvm::APSInt& V) {
   // Create a new state with the old binding replaced.
-  return state->set<ConstEq>(sym, &V);
+  return state->set<ConstEq>(sym, &state->getBasicVals().getValue(V));
 }
 
 const GRState* BasicConstraintManager::AddNE(const GRState* state, SymbolRef sym,
@@ -224,7 +240,7 @@
   GRState::IntSetTy S = T ? *T : ISetFactory.GetEmptySet();
 
   // Now add V to the NE set.
-  S = ISetFactory.Add(S, &V);
+  S = ISetFactory.Add(S, &state->getBasicVals().getValue(V));
 
   // Create a new state with the old binding replaced.
   return state->set<ConstNotEq>(sym, S);
@@ -243,7 +259,7 @@
   const ConstNotEqTy::data_type* T = state->get<ConstNotEq>(sym);
 
   // See if V is present in the NE-set.
-  return T ? T->contains(&V) : false;
+  return T ? T->contains(&state->getBasicVals().getValue(V)) : false;
 }
 
 bool BasicConstraintManager::isEqual(const GRState* state, SymbolRef sym,
diff --git a/lib/Checker/RangeConstraintManager.cpp b/lib/Checker/RangeConstraintManager.cpp
index c904c33..2a35d32 100644
--- a/lib/Checker/RangeConstraintManager.cpp
+++ b/lib/Checker/RangeConstraintManager.cpp
@@ -105,97 +105,69 @@
     return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : 0;
   }
 
-  /// AddEQ - Create a new RangeSet with the additional constraint that the
-  ///  value be equal to V.
-  RangeSet AddEQ(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
-    // Search for a range that includes 'V'.  If so, return a new RangeSet
-    // representing { [V, V] }.
-    for (PrimRangeSet::iterator i = begin(), e = end(); i!=e; ++i)
-      if (i->Includes(V))
-        return RangeSet(F, V, V);
-
-    return RangeSet(F);
-  }
-
-  /// AddNE - Create a new RangeSet with the additional constraint that the
-  ///  value be not be equal to V.
-  RangeSet AddNE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
-    PrimRangeSet newRanges = ranges;
-
-    // FIXME: We can perhaps enhance ImmutableSet to do this search for us
-    // in log(N) time using the sorted property of the internal AVL tree.
-    for (iterator i = begin(), e = end(); i != e; ++i) {
-      if (i->Includes(V)) {
-        // Remove the old range.
-        newRanges = F.Remove(newRanges, *i);
-        // Split the old range into possibly one or two ranges.
-        if (V != i->From())
-          newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V)));
-        if (V != i->To())
-          newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To()));
-        // All of the ranges are non-overlapping, so we can stop.
+private:
+  void IntersectInRange(BasicValueFactory &BV, Factory &F,
+                        const llvm::APSInt &Lower,
+                        const llvm::APSInt &Upper,
+                        PrimRangeSet &newRanges,
+                        PrimRangeSet::iterator &i,
+                        PrimRangeSet::iterator &e) const {
+    // There are six cases for each range R in the set:
+    //   1. R is entirely before the intersection range.
+    //   2. R is entirely after the intersection range.
+    //   3. R contains the entire intersection range.
+    //   4. R starts before the intersection range and ends in the middle.
+    //   5. R starts in the middle of the intersection range and ends after it.
+    //   6. R is entirely contained in the intersection range.
+    // These correspond to each of the conditions below.
+    for (/* i = begin(), e = end() */; i != e; ++i) {
+      if (i->To() < Lower) {
+        continue;
+      }
+      if (i->From() > Upper) {
         break;
       }
-    }
 
-    return newRanges;
+      if (i->Includes(Lower)) {
+        if (i->Includes(Upper)) {
+          newRanges = F.Add(newRanges, Range(BV.getValue(Lower),
+                                             BV.getValue(Upper)));
+          break;
+        } else
+          newRanges = F.Add(newRanges, Range(BV.getValue(Lower), i->To()));
+      } else {
+        if (i->Includes(Upper)) {
+          newRanges = F.Add(newRanges, Range(i->From(), BV.getValue(Upper)));
+          break;
+        } else
+          newRanges = F.Add(newRanges, *i);
+      }
+    }
   }
 
-  /// AddNE - Create a new RangeSet with the additional constraint that the
-  ///  value be less than V.
-  RangeSet AddLT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
+public:
+  // Returns a set containing the values in the receiving set, intersected with
+  // the closed range [Lower, Upper]. Unlike the Range type, this range uses
+  // modular arithmetic, corresponding to the common treatment of C integer
+  // overflow. Thus, if the Lower bound is greater than the Upper bound, the
+  // range is taken to wrap around. This is equivalent to taking the
+  // intersection with the two ranges [Min, Upper] and [Lower, Max],
+  // or, alternatively, /removing/ all integers between Upper and Lower.
+  RangeSet Intersect(BasicValueFactory &BV, Factory &F,
+                     const llvm::APSInt &Lower,
+                     const llvm::APSInt &Upper) const {
     PrimRangeSet newRanges = F.GetEmptySet();
 
-    for (iterator i = begin(), e = end() ; i != e ; ++i) {
-      if (i->Includes(V) && i->From() < V)
-        newRanges = F.Add(newRanges, Range(i->From(), BV.Sub1(V)));
-      else if (i->To() < V)
-        newRanges = F.Add(newRanges, *i);
+    PrimRangeSet::iterator i = begin(), e = end();
+    if (Lower <= Upper)
+      IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
+    else {
+      // The order of the next two statements is important!
+      // IntersectInRange() does not reset the iteration state for i and e.
+      // Therefore, the lower range most be handled first.
+      IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
+      IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
     }
-
-    return newRanges;
-  }
-
-  RangeSet AddLE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
-    PrimRangeSet newRanges = F.GetEmptySet();
-
-    for (iterator i = begin(), e = end(); i != e; ++i) {
-      // Strictly we should test for includes *V + 1, but no harm is
-      // done by this formulation
-      if (i->Includes(V))
-        newRanges = F.Add(newRanges, Range(i->From(), V));
-      else if (i->To() <= V)
-        newRanges = F.Add(newRanges, *i);
-    }
-
-    return newRanges;
-  }
-
-  RangeSet AddGT(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
-    PrimRangeSet newRanges = F.GetEmptySet();
-
-    for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) {
-      if (i->Includes(V) && i->To() > V)
-        newRanges = F.Add(newRanges, Range(BV.Add1(V), i->To()));
-      else if (i->From() > V)
-        newRanges = F.Add(newRanges, *i);
-    }
-
-    return newRanges;
-  }
-
-  RangeSet AddGE(BasicValueFactory &BV, Factory &F, const llvm::APSInt &V) {
-    PrimRangeSet newRanges = F.GetEmptySet();
-
-    for (PrimRangeSet::iterator i = begin(), e = end(); i != e; ++i) {
-      // Strictly we should test for includes *V - 1, but no harm is
-      // done by this formulation
-      if (i->Includes(V))
-        newRanges = F.Add(newRanges, Range(V, i->To()));
-      else if (i->From() >= V)
-        newRanges = F.Add(newRanges, *i);
-    }
-
     return newRanges;
   }
 
@@ -237,23 +209,29 @@
   RangeConstraintManager(GRSubEngine &subengine)
     : SimpleConstraintManager(subengine) {}
 
-  const GRState* AssumeSymNE(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymNE(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
-  const GRState* AssumeSymEQ(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymEQ(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
-  const GRState* AssumeSymLT(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymLT(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
-  const GRState* AssumeSymGT(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymGT(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
-  const GRState* AssumeSymGE(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymGE(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
-  const GRState* AssumeSymLE(const GRState* St, SymbolRef sym,
-                             const llvm::APSInt& V);
+  const GRState* AssumeSymLE(const GRState* state, SymbolRef sym,
+                             const llvm::APSInt& Int,
+                             const llvm::APSInt& Adjustment);
 
   const llvm::APSInt* getSymVal(const GRState* St, SymbolRef sym) const;
 
@@ -303,10 +281,6 @@
   return state->set<ConstraintRange>(CR);
 }
 
-//===------------------------------------------------------------------------===
-// AssumeSymX methods: public interface for RangeConstraintManager.
-//===------------------------------------------------------------------------===/
-
 RangeSet
 RangeConstraintManager::GetRange(const GRState *state, SymbolRef sym) {
   if (ConstraintRangeTy::data_type* V = state->get<ConstraintRange>(sym))
@@ -323,20 +297,127 @@
 // AssumeSymX methods: public interface for RangeConstraintManager.
 //===------------------------------------------------------------------------===/
 
-#define AssumeX(OP)\
-const GRState*\
-RangeConstraintManager::AssumeSym ## OP(const GRState* state, SymbolRef sym,\
-  const llvm::APSInt& V){\
-  const RangeSet& R = GetRange(state, sym).Add##OP(state->getBasicVals(), F, V);\
-  return !R.isEmpty() ? state->set<ConstraintRange>(sym, R) : NULL;\
+// The syntax for ranges below is mathematical, using [x, y] for closed ranges
+// and (x, y) for open ranges. These ranges are modular, corresponding with
+// a common treatment of C integer overflow. This means that these methods
+// do not have to worry about overflow; RangeSet::Intersect can handle such a
+// "wraparound" range.
+// As an example, the range [UINT_MAX-1, 3) contains five values: UINT_MAX-1,
+// UINT_MAX, 0, 1, and 2.
+
+const GRState*
+RangeConstraintManager::AssumeSymNE(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Upper = Lower;
+  --Lower;
+  ++Upper;
+
+  // [Int-Adjustment+1, Int-Adjustment-1]
+  // Notice that the lower bound is greater than the upper bound.
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Upper, Lower);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
 }
 
-AssumeX(EQ)
-AssumeX(NE)
-AssumeX(LT)
-AssumeX(GT)
-AssumeX(LE)
-AssumeX(GE)
+const GRState*
+RangeConstraintManager::AssumeSymEQ(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  // [Int-Adjustment, Int-Adjustment]
+  BasicValueFactory &BV = state->getBasicVals();
+  llvm::APSInt AdjInt = Int-Adjustment;
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, AdjInt, AdjInt);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymLT(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  QualType T = state->getSymbolManager().getType(sym);
+  const llvm::APSInt &Min = BV.getMinValue(T);
+
+  // Special case for Int == Min. This is always false.
+  if (Int == Min)
+    return NULL;
+
+  llvm::APSInt Lower = Min-Adjustment;
+  llvm::APSInt Upper = Int-Adjustment;
+  --Upper;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymGT(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  QualType T = state->getSymbolManager().getType(sym);
+  const llvm::APSInt &Max = BV.getMaxValue(T);
+
+  // Special case for Int == Max. This is always false.
+  if (Int == Max)
+    return NULL;
+
+  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Upper = Max-Adjustment;
+  ++Lower;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymGE(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  QualType T = state->getSymbolManager().getType(sym);
+  const llvm::APSInt &Min = BV.getMinValue(T);
+
+  // Special case for Int == Min. This is always feasible.
+  if (Int == Min)
+    return state;
+
+  const llvm::APSInt &Max = BV.getMaxValue(T);
+
+  llvm::APSInt Lower = Int-Adjustment;
+  llvm::APSInt Upper = Max-Adjustment;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
+
+const GRState*
+RangeConstraintManager::AssumeSymLE(const GRState* state, SymbolRef sym,
+                                    const llvm::APSInt& Int,
+                                    const llvm::APSInt& Adjustment) {
+  BasicValueFactory &BV = state->getBasicVals();
+
+  QualType T = state->getSymbolManager().getType(sym);
+  const llvm::APSInt &Max = BV.getMaxValue(T);
+
+  // Special case for Int == Max. This is always feasible.
+  if (Int == Max)
+    return state;
+
+  const llvm::APSInt &Min = BV.getMinValue(T);
+
+  llvm::APSInt Lower = Min-Adjustment;
+  llvm::APSInt Upper = Int-Adjustment;
+
+  RangeSet New = GetRange(state, sym).Intersect(BV, F, Lower, Upper);
+  return New.isEmpty() ? NULL : state->set<ConstraintRange>(sym, New);
+}
 
 //===------------------------------------------------------------------------===
 // Pretty-printing.
diff --git a/lib/Checker/SimpleConstraintManager.cpp b/lib/Checker/SimpleConstraintManager.cpp
index 8c423a9..3d6930b 100644
--- a/lib/Checker/SimpleConstraintManager.cpp
+++ b/lib/Checker/SimpleConstraintManager.cpp
@@ -35,12 +35,11 @@
         case BinaryOperator::Or:
         case BinaryOperator::Xor:
           return false;
-        // We don't reason yet about arithmetic constraints on symbolic values.
+        // We don't reason yet about these arithmetic constraints on
+        // symbolic values.
         case BinaryOperator::Mul:
         case BinaryOperator::Div:
         case BinaryOperator::Rem:
-        case BinaryOperator::Add:
-        case BinaryOperator::Sub:
         case BinaryOperator::Shl:
         case BinaryOperator::Shr:
           return false;
@@ -90,12 +89,11 @@
     while (SubR) {
       // FIXME: now we only find the first symbolic region.
       if (const SymbolicRegion *SymR = dyn_cast<SymbolicRegion>(SubR)) {
+        const llvm::APSInt &zero = BasicVals.getZeroWithPtrWidth();
         if (Assumption)
-          return AssumeSymNE(state, SymR->getSymbol(),
-                             BasicVals.getZeroWithPtrWidth());
+          return AssumeSymNE(state, SymR->getSymbol(), zero, zero);
         else
-          return AssumeSymEQ(state, SymR->getSymbol(),
-                             BasicVals.getZeroWithPtrWidth());
+          return AssumeSymEQ(state, SymR->getSymbol(), zero, zero);
       }
       SubR = dyn_cast<SubRegion>(SubR->getSuperRegion());
     }
@@ -121,11 +119,27 @@
   return SU.ProcessAssume(state, cond, assumption);
 }
 
+static BinaryOperator::Opcode NegateComparison(BinaryOperator::Opcode op) {
+  // FIXME: This should probably be part of BinaryOperator, since this isn't
+  // the only place it's used. (This code was copied from SimpleSValuator.cpp.)
+  switch (op) {
+  default:
+    assert(false && "Invalid opcode.");
+  case BinaryOperator::LT: return BinaryOperator::GE;
+  case BinaryOperator::GT: return BinaryOperator::LE;
+  case BinaryOperator::LE: return BinaryOperator::GT;
+  case BinaryOperator::GE: return BinaryOperator::LT;
+  case BinaryOperator::EQ: return BinaryOperator::NE;
+  case BinaryOperator::NE: return BinaryOperator::EQ;
+  }
+}
+
 const GRState *SimpleConstraintManager::AssumeAux(const GRState *state,
                                                   NonLoc Cond,
                                                   bool Assumption) {
 
-  // We cannot reason about SymIntExpr and SymSymExpr.
+  // We cannot reason about SymSymExprs,
+  // and can only reason about some SymIntExprs.
   if (!canReasonAbout(Cond)) {
     // Just return the current state indicating that the path is feasible.
     // This may be an over-approximation of what is possible.
@@ -144,30 +158,42 @@
     SymbolRef sym = SV.getSymbol();
     QualType T =  SymMgr.getType(sym);
     const llvm::APSInt &zero = BasicVals.getValue(0, T);
-
-    return Assumption ? AssumeSymNE(state, sym, zero)
-                      : AssumeSymEQ(state, sym, zero);
+    if (Assumption)
+      return AssumeSymNE(state, sym, zero, zero);
+    else
+      return AssumeSymEQ(state, sym, zero, zero);
   }
 
   case nonloc::SymExprValKind: {
     nonloc::SymExprVal V = cast<nonloc::SymExprVal>(Cond);
-    if (const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression())){
-      // FIXME: This is a hack.  It silently converts the RHS integer to be
-      // of the same type as on the left side.  This should be removed once
-      // we support truncation/extension of symbolic values.      
-      GRStateManager &StateMgr = state->getStateManager();
-      ASTContext &Ctx = StateMgr.getContext();
-      QualType LHSType = SE->getLHS()->getType(Ctx);
-      BasicValueFactory &BasicVals = StateMgr.getBasicVals();
-      const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
-      SymIntExpr SENew(SE->getLHS(), SE->getOpcode(), RHS, SE->getType(Ctx));
 
-      return AssumeSymInt(state, Assumption, &SENew);
-    }
+    // For now, we only handle expressions whose RHS is an integer.
+    // All other expressions are assumed to be feasible.
+    const SymIntExpr *SE = dyn_cast<SymIntExpr>(V.getSymbolicExpression());
+    if (!SE)
+      return state;
 
-    // For all other symbolic expressions, over-approximate and consider
-    // the constraint feasible.
-    return state;
+    GRStateManager &StateMgr = state->getStateManager();
+    ASTContext &Ctx = StateMgr.getContext();
+    BasicValueFactory &BasicVals = StateMgr.getBasicVals();
+
+    // FIXME: This is a hack.  It silently converts the RHS integer to be
+    // of the same type as on the left side.  This should be removed once
+    // we support truncation/extension of symbolic values.   
+    const SymExpr *LHS = SE->getLHS();
+    QualType LHSType = LHS->getType(Ctx);
+    const llvm::APSInt &RHS = BasicVals.Convert(LHSType, SE->getRHS());
+
+    BinaryOperator::Opcode op = SE->getOpcode();
+    // FIXME: We should implicitly compare non-comparison expressions to 0.
+    if (!BinaryOperator::isComparisonOp(op))
+      return state;
+
+    // From here on out, op is the real comparison we'll be testing.
+    if (!Assumption)
+      op = NegateComparison(op);
+  
+    return AssumeSymRel(state, LHS, op, RHS);
   }
 
   case nonloc::ConcreteIntKind: {
@@ -182,43 +208,76 @@
   } // end switch
 }
 
-const GRState *SimpleConstraintManager::AssumeSymInt(const GRState *state,
-                                                     bool Assumption,
-                                                     const SymIntExpr *SE) {
+const GRState *SimpleConstraintManager::AssumeSymRel(const GRState *state,
+                                                     const SymExpr *LHS,
+                                                     BinaryOperator::Opcode op,
+                                                     const llvm::APSInt& Int) {
+  assert(BinaryOperator::isComparisonOp(op) &&
+         "Non-comparison ops should be rewritten as comparisons to zero.");
 
+   // We only handle simple comparisons of the form "$sym == constant"
+   // or "($sym+constant1) == constant2".
+   // The adjustment is "constant1" in the above expression. It's used to
+   // "slide" the solution range around for modular arithmetic. For example,
+   // x < 4 has the solution [0, 3]. x+2 < 4 has the solution [0-2, 3-2], which
+   // in modular arithmetic is [0, 1] U [UINT_MAX-1, UINT_MAX]. It's up to
+   // the subclasses of SimpleConstraintManager to handle the adjustment.
+   llvm::APSInt Adjustment(Int.getBitWidth(), Int.isUnsigned());
 
-  // Here we assume that LHS is a symbol.  This is consistent with the
-  // rest of the constraint manager logic.
-  SymbolRef Sym = cast<SymbolData>(SE->getLHS());
-  const llvm::APSInt &Int = SE->getRHS();
+  // First check if the LHS is a simple symbol reference.
+  SymbolRef Sym = dyn_cast<SymbolData>(LHS);
+  if (!Sym) {
+    // Next, see if it's a "($sym+constant1)" expression.
+    const SymIntExpr *SE = dyn_cast<SymIntExpr>(LHS);
 
-  switch (SE->getOpcode()) {
+    // We don't handle "($sym1+$sym2)".
+    // Give up and assume the constraint is feasible.
+    if (!SE)
+      return state;
+
+    // We don't handle "(<expr>+constant1)".
+    // Give up and assume the constraint is feasible.
+    Sym = dyn_cast<SymbolData>(SE->getLHS());
+    if (!Sym)
+      return state;
+
+    // Get the constant out of the expression "($sym+constant1)".
+    switch (SE->getOpcode()) {
+    case BinaryOperator::Add:
+      Adjustment = SE->getRHS();
+      break;
+    case BinaryOperator::Sub:
+      Adjustment = -SE->getRHS();
+      break;
+    default:
+      // We don't handle non-additive operators.
+      // Give up and assume the constraint is feasible.
+      return state;
+    }
+  }
+
+  switch (op) {
   default:
     // No logic yet for other operators.  Assume the constraint is feasible.
     return state;
 
   case BinaryOperator::EQ:
-    return Assumption ? AssumeSymEQ(state, Sym, Int)
-                      : AssumeSymNE(state, Sym, Int);
+    return AssumeSymEQ(state, Sym, Int, Adjustment);
 
   case BinaryOperator::NE:
-    return Assumption ? AssumeSymNE(state, Sym, Int)
-                      : AssumeSymEQ(state, Sym, Int);
+    return AssumeSymNE(state, Sym, Int, Adjustment);
+
   case BinaryOperator::GT:
-    return Assumption ? AssumeSymGT(state, Sym, Int)
-                      : AssumeSymLE(state, Sym, Int);
+    return AssumeSymGT(state, Sym, Int, Adjustment);
 
   case BinaryOperator::GE:
-    return Assumption ? AssumeSymGE(state, Sym, Int)
-                      : AssumeSymLT(state, Sym, Int);
+    return AssumeSymGE(state, Sym, Int, Adjustment);
 
   case BinaryOperator::LT:
-    return Assumption ? AssumeSymLT(state, Sym, Int)
-                      : AssumeSymGE(state, Sym, Int);
+    return AssumeSymLT(state, Sym, Int, Adjustment);
 
   case BinaryOperator::LE:
-    return Assumption ? AssumeSymLE(state, Sym, Int)
-                      : AssumeSymGT(state, Sym, Int);
+    return AssumeSymLE(state, Sym, Int, Adjustment);
   } // end switch
 }
 
diff --git a/lib/Checker/SimpleConstraintManager.h b/lib/Checker/SimpleConstraintManager.h
index 5f20e00..45057e6 100644
--- a/lib/Checker/SimpleConstraintManager.h
+++ b/lib/Checker/SimpleConstraintManager.h
@@ -38,8 +38,10 @@
 
   const GRState *Assume(const GRState *state, NonLoc Cond, bool Assumption);
 
-  const GRState *AssumeSymInt(const GRState *state, bool Assumption,
-                              const SymIntExpr *SE);
+  const GRState *AssumeSymRel(const GRState *state,
+                              const SymExpr *LHS,
+                              BinaryOperator::Opcode op,
+                              const llvm::APSInt& Int);
 
   const GRState *AssumeInBound(const GRState *state, DefinedSVal Idx,
                                DefinedSVal UpperBound,
@@ -51,23 +53,31 @@
   // Interface that subclasses must implement.
   //===------------------------------------------------------------------===//
 
+  // Each of these is of the form "$sym+Adj <> V", where "<>" is the comparison
+  // operation for the method being invoked.
   virtual const GRState *AssumeSymNE(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   virtual const GRState *AssumeSymEQ(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   virtual const GRState *AssumeSymLT(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   virtual const GRState *AssumeSymGT(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   virtual const GRState *AssumeSymLE(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   virtual const GRState *AssumeSymGE(const GRState *state, SymbolRef sym,
-                                     const llvm::APSInt& V) = 0;
+                                     const llvm::APSInt& V,
+                                     const llvm::APSInt& Adjustment) = 0;
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
diff --git a/lib/Checker/SimpleSValuator.cpp b/lib/Checker/SimpleSValuator.cpp
index dd38a43..c85d038 100644
--- a/lib/Checker/SimpleSValuator.cpp
+++ b/lib/Checker/SimpleSValuator.cpp
@@ -261,63 +261,88 @@
       }
     }
     case nonloc::SymExprValKind: {
-      // Logical not?
-      if (!(op == BinaryOperator::EQ && rhs.isZeroConstant()))
+      nonloc::SymExprVal *selhs = cast<nonloc::SymExprVal>(&lhs);
+
+      // Only handle LHS of the form "$sym op constant", at least for now.
+      const SymIntExpr *symIntExpr =
+        dyn_cast<SymIntExpr>(selhs->getSymbolicExpression());
+
+      if (!symIntExpr)
         return UnknownVal();
 
-      const SymExpr *symExpr =
-        cast<nonloc::SymExprVal>(lhs).getSymbolicExpression();
+      // Is this a logical not? (!x is represented as x == 0.)
+      if (op == BinaryOperator::EQ && rhs.isZeroConstant()) {
+        // We know how to negate certain expressions. Simplify them here.
 
-      // Only handle ($sym op constant) for now.
-      if (const SymIntExpr *symIntExpr = dyn_cast<SymIntExpr>(symExpr)) {
         BinaryOperator::Opcode opc = symIntExpr->getOpcode();
         switch (opc) {
-          case BinaryOperator::LAnd:
-          case BinaryOperator::LOr:
-            assert(false && "Logical operators handled by branching logic.");
-            return UnknownVal();
-          case BinaryOperator::Assign:
-          case BinaryOperator::MulAssign:
-          case BinaryOperator::DivAssign:
-          case BinaryOperator::RemAssign:
-          case BinaryOperator::AddAssign:
-          case BinaryOperator::SubAssign:
-          case BinaryOperator::ShlAssign:
-          case BinaryOperator::ShrAssign:
-          case BinaryOperator::AndAssign:
-          case BinaryOperator::XorAssign:
-          case BinaryOperator::OrAssign:
-          case BinaryOperator::Comma:
-            assert(false && "'=' and ',' operators handled by GRExprEngine.");
-            return UnknownVal();
-          case BinaryOperator::PtrMemD:
-          case BinaryOperator::PtrMemI:
-            assert(false && "Pointer arithmetic not handled here.");
-            return UnknownVal();
-          case BinaryOperator::Mul:
-          case BinaryOperator::Div:
-          case BinaryOperator::Rem:
-          case BinaryOperator::Add:
-          case BinaryOperator::Sub:
-          case BinaryOperator::Shl:
-          case BinaryOperator::Shr:
-          case BinaryOperator::And:
-          case BinaryOperator::Xor:
-          case BinaryOperator::Or:
-            // Not handled yet.
-            return UnknownVal();
-          case BinaryOperator::LT:
-          case BinaryOperator::GT:
-          case BinaryOperator::LE:
-          case BinaryOperator::GE:
-          case BinaryOperator::EQ:
-          case BinaryOperator::NE:
-            opc = NegateComparison(opc);
-            assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
-            return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
-                                     symIntExpr->getRHS(), resultTy);
+        default:
+          // We don't know how to negate this operation.
+          // Just handle it as if it were a normal comparison to 0.
+          break;
+        case BinaryOperator::LAnd:
+        case BinaryOperator::LOr:
+          assert(false && "Logical operators handled by branching logic.");
+          return UnknownVal();
+        case BinaryOperator::Assign:
+        case BinaryOperator::MulAssign:
+        case BinaryOperator::DivAssign:
+        case BinaryOperator::RemAssign:
+        case BinaryOperator::AddAssign:
+        case BinaryOperator::SubAssign:
+        case BinaryOperator::ShlAssign:
+        case BinaryOperator::ShrAssign:
+        case BinaryOperator::AndAssign:
+        case BinaryOperator::XorAssign:
+        case BinaryOperator::OrAssign:
+        case BinaryOperator::Comma:
+          assert(false && "'=' and ',' operators handled by GRExprEngine.");
+          return UnknownVal();
+        case BinaryOperator::PtrMemD:
+        case BinaryOperator::PtrMemI:
+          assert(false && "Pointer arithmetic not handled here.");
+          return UnknownVal();
+        case BinaryOperator::LT:
+        case BinaryOperator::GT:
+        case BinaryOperator::LE:
+        case BinaryOperator::GE:
+        case BinaryOperator::EQ:
+        case BinaryOperator::NE:
+          // Negate the comparison and make a value.
+          opc = NegateComparison(opc);
+          assert(symIntExpr->getType(ValMgr.getContext()) == resultTy);
+          return ValMgr.makeNonLoc(symIntExpr->getLHS(), opc,
+                                   symIntExpr->getRHS(), resultTy);
         }
       }
+
+      // For now, only handle expressions whose RHS is a constant.
+      const nonloc::ConcreteInt *rhsInt = dyn_cast<nonloc::ConcreteInt>(&rhs);
+      if (!rhsInt)
+        return UnknownVal();
+
+      // If both the LHS and the current expression are additive,
+      // fold their constants.
+      if (BinaryOperator::isAdditiveOp(op)) {
+        BinaryOperator::Opcode lop = symIntExpr->getOpcode();
+        if (BinaryOperator::isAdditiveOp(lop)) {
+          BasicValueFactory &BVF = ValMgr.getBasicValueFactory();
+          const llvm::APSInt *newRHS;
+          if (lop == op)
+            newRHS = BVF.EvaluateAPSInt(BinaryOperator::Add,
+                                        symIntExpr->getRHS(),
+                                        rhsInt->getValue());
+          else
+            newRHS = BVF.EvaluateAPSInt(BinaryOperator::Sub,
+                                        symIntExpr->getRHS(),
+                                        rhsInt->getValue());
+          return ValMgr.makeNonLoc(symIntExpr->getLHS(), lop, *newRHS,
+                                   resultTy);
+        }
+      }
+
+      // Otherwise, make a SymExprVal out of the expression.
+      return ValMgr.makeNonLoc(symIntExpr, op, rhsInt->getValue(), resultTy);
     }
     case nonloc::ConcreteIntKind: {
       if (isa<nonloc::ConcreteInt>(rhs)) {