diff --git a/lib/Analysis/GRSimpleVals.cpp b/lib/Analysis/GRSimpleVals.cpp
index e2dde76..22ccd7b 100644
--- a/lib/Analysis/GRSimpleVals.cpp
+++ b/lib/Analysis/GRSimpleVals.cpp
@@ -230,11 +230,16 @@
         
       case nonloc::SymbolValKind:
         if (isa<nonloc::ConcreteInt>(R)) {
-          const SymIntConstraint& C =
-            BasicVals.getConstraint(cast<nonloc::SymbolVal>(L).getSymbol(), Op,
-                                    cast<nonloc::ConcreteInt>(R).getValue());
-          
-          return nonloc::SymIntConstraintVal(C);
+          if (Op >= BinaryOperator::LT && Op <= BinaryOperator::NE) {
+            const SymIntConstraint& C =
+              BasicVals.getConstraint(cast<nonloc::SymbolVal>(L).getSymbol(), 
+                                   Op, cast<nonloc::ConcreteInt>(R).getValue());
+            return nonloc::SymIntConstraintVal(C);
+          } else {
+            return NonLoc::MakeVal(Eng.getSymbolManager(),
+                                   cast<nonloc::SymbolVal>(L).getSymbol(),
+                                   Op, cast<nonloc::ConcreteInt>(R).getValue());
+          }
         }
         else
           return UnknownVal();
diff --git a/lib/Analysis/SVals.cpp b/lib/Analysis/SVals.cpp
index 12bf795..0f34560 100644
--- a/lib/Analysis/SVals.cpp
+++ b/lib/Analysis/SVals.cpp
@@ -283,6 +283,23 @@
   return nonloc::SymbolVal(sym);
 }
 
+NonLoc NonLoc::MakeVal(SymbolManager& SymMgr, SymbolRef lhs, 
+                       BinaryOperator::Opcode op, const APSInt& v) {
+  // The Environment ensures we always get a persistent APSInt in
+  // BasicValueFactory, so we don't need to get the APSInt from
+  // BasicValueFactory again.
+
+  SymbolRef sym = SymMgr.getSymIntExpr(lhs, op, v, SymMgr.getType(lhs));
+  return nonloc::SymbolVal(sym);
+}
+
+NonLoc NonLoc::MakeVal(SymbolManager& SymMgr, SymbolRef lhs, 
+                       BinaryOperator::Opcode op, SymbolRef rhs) {
+  assert(SymMgr.getType(lhs) == SymMgr.getType(rhs));
+  SymbolRef sym = SymMgr.getSymSymExpr(lhs, op, rhs, SymMgr.getType(lhs));
+  return nonloc::SymbolVal(sym);
+}
+
 NonLoc NonLoc::MakeIntVal(BasicValueFactory& BasicVals, uint64_t X, 
                           bool isUnsigned) {
   return nonloc::ConcreteInt(BasicVals.getIntValue(X, isUnsigned));
diff --git a/lib/Analysis/SimpleConstraintManager.cpp b/lib/Analysis/SimpleConstraintManager.cpp
index e6f940e..50552c1 100644
--- a/lib/Analysis/SimpleConstraintManager.cpp
+++ b/lib/Analysis/SimpleConstraintManager.cpp
@@ -21,28 +21,11 @@
 SimpleConstraintManager::~SimpleConstraintManager() {}
 
 bool SimpleConstraintManager::canReasonAbout(SVal X) const {
-  if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) {
-    const SymIntConstraint& C = Y->getConstraint();
-    switch (C.getOpcode()) {
-        // We don't reason yet about bitwise-constraints on symbolic values.
-      case BinaryOperator::And:
-      case BinaryOperator::Or:
-      case BinaryOperator::Xor:
-        return false;
-        // We don't reason yet about 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;
-
-        // All other cases.
-      default:
-        return true;
-    }
+  if (nonloc::SymbolVal* SymVal = dyn_cast<nonloc::SymbolVal>(&X)) {
+    const SymbolData& data 
+      = getSymbolManager().getSymbolData(SymVal->getSymbol());
+    return !(data.getKind() == SymbolData::SymIntKind || 
+             data.getKind() == SymbolData::SymSymKind );
   }
 
   return true;
@@ -143,6 +126,12 @@
 const GRState*
 SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond,
                                    bool Assumption, bool& isFeasible) {
+  // We cannot reason about SymIntExpr and SymSymExpr.
+  if (!canReasonAbout(Cond)) {
+    isFeasible = true;
+    return St;
+  }  
+
   BasicValueFactory& BasicVals = StateMgr.getBasicVals();
   SymbolManager& SymMgr = StateMgr.getSymbolManager();
 
diff --git a/lib/Analysis/SimpleConstraintManager.h b/lib/Analysis/SimpleConstraintManager.h
index 08ab660..8195c8e 100644
--- a/lib/Analysis/SimpleConstraintManager.h
+++ b/lib/Analysis/SimpleConstraintManager.h
@@ -76,6 +76,7 @@
 
 private:
   BasicValueFactory& getBasicVals() { return StateMgr.getBasicVals(); }
+  SymbolManager& getSymbolManager() const { return StateMgr.getSymbolManager(); }
 };
 
 }  // end clang namespace
diff --git a/lib/Analysis/SymbolManager.cpp b/lib/Analysis/SymbolManager.cpp
index efc7cd3..33d6a57 100644
--- a/lib/Analysis/SymbolManager.cpp
+++ b/lib/Analysis/SymbolManager.cpp
@@ -74,6 +74,47 @@
   return SymbolCounter++;
 }
 
+SymbolRef SymbolManager::getSymIntExpr(SymbolRef lhs,BinaryOperator::Opcode op, 
+                                       const llvm::APSInt& v, QualType t) {
+  llvm::FoldingSetNodeID ID;
+  SymIntExpr::Profile(ID, lhs, op, v, t);
+  void* InsertPos;
+
+  SymbolData* data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
+
+  if (data)
+    return data->getSymbol();
+
+  data = (SymIntExpr*) BPAlloc.Allocate<SymIntExpr>();
+  new (data) SymIntExpr(SymbolCounter, lhs, op, v, t);
+
+  DataSet.InsertNode(data, InsertPos);
+  DataMap[SymbolCounter] = data;
+
+  return SymbolCounter++;
+}
+
+SymbolRef SymbolManager::getSymSymExpr(SymbolRef lhs, BinaryOperator::Opcode op,
+                                       SymbolRef rhs, QualType t) {
+  llvm::FoldingSetNodeID ID;
+  SymSymExpr::Profile(ID, lhs, op, rhs, t);
+  void* InsertPos;
+
+  SymbolData* data = DataSet.FindNodeOrInsertPos(ID, InsertPos);
+
+  if (data)
+    return data->getSymbol();
+
+  data = (SymSymExpr*) BPAlloc.Allocate<SymSymExpr>();
+  new (data) SymSymExpr(SymbolCounter, lhs, op, rhs, t);
+
+  DataSet.InsertNode(data, InsertPos);
+  DataMap[SymbolCounter] = data;
+
+  return SymbolCounter++;
+}
+
+
 const SymbolData& SymbolManager::getSymbolData(SymbolRef Sym) const {  
   DataMapTy::const_iterator I = DataMap.find(Sym);
   assert (I != DataMap.end());