diff --git a/Analysis/GRConstants.cpp b/Analysis/GRConstants.cpp
index d841eec..5116499 100644
--- a/Analysis/GRConstants.cpp
+++ b/Analysis/GRConstants.cpp
@@ -228,6 +228,12 @@
   StateTy Assume(StateTy St, LValue Cond, bool Assumption, bool& isFeasible);
   StateTy Assume(StateTy St, NonLValue Cond, bool Assumption, bool& isFeasible);
   
+  StateTy AssumeSymNE(StateTy St, SymbolID sym, const llvm::APSInt& V,
+                      bool& isFeasible);
+
+  StateTy AssumeSymEQ(StateTy St, SymbolID sym, const llvm::APSInt& V,
+                      bool& isFeasible);
+  
   void Nodify(NodeSet& Dst, Stmt* S, NodeTy* Pred, StateTy St);
   
   /// Nodify - This version of Nodify is used to batch process a set of states.
@@ -851,18 +857,27 @@
 // "Assume" logic.
 //===----------------------------------------------------------------------===//
 
-GRConstants::StateTy GRConstants::Assume(StateTy St, LValue Cond, bool Assumption, 
+GRConstants::StateTy GRConstants::Assume(StateTy St, LValue Cond,
+                                         bool Assumption, 
                                          bool& isFeasible) {    
   
   switch (Cond.getSubKind()) {
     default:
-      assert (false && "'Assume' not implemented for this NonLValue.");
+      assert (false && "'Assume' not implemented for this LValue.");
       return St;
       
+    case lval::SymbolValKind:
+      if (Assumption)
+        return AssumeSymNE(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                           ValMgr.getZeroWithPtrWidth(), isFeasible);
+      else
+        return AssumeSymEQ(St, cast<lval::SymbolVal>(Cond).getSymbol(),
+                           ValMgr.getZeroWithPtrWidth(), isFeasible);
+      
     case lval::DeclValKind:
       isFeasible = Assumption;
       return St;
-      
+
     case lval::ConcreteIntKind: {
       bool b = cast<lval::ConcreteInt>(Cond).getValue() != 0;
       isFeasible = b ? Assumption : !Assumption;      
@@ -871,7 +886,8 @@
   }
 }
 
-GRConstants::StateTy GRConstants::Assume(StateTy St, NonLValue Cond, bool Assumption, 
+GRConstants::StateTy GRConstants::Assume(StateTy St, NonLValue Cond,
+                                         bool Assumption, 
                                          bool& isFeasible) {
   
   switch (Cond.getSubKind()) {
@@ -887,6 +903,51 @@
   }
 }
 
+GRConstants::StateTy
+GRConstants::AssumeSymNE(StateTy St, SymbolID sym,
+                         const llvm::APSInt& V, bool& isFeasible) {
+
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St.getSymVal(sym)) {
+    isFeasible = *X != V;
+    return St;
+  }
+  
+  // Second, determine if sym != V.
+  if (St.isNotEqual(sym, V)) {
+    isFeasible = true;
+    return St;
+  }
+      
+  // If we reach here, sym is not a constant and we don't know if it is != V.
+  // Make that assumption.
+  
+  isFeasible = true;
+  return StateMgr.AddNE(St, sym, V);
+}
+
+GRConstants::StateTy
+GRConstants::AssumeSymEQ(StateTy St, SymbolID sym,
+                         const llvm::APSInt& V, bool& isFeasible) {
+  
+  // First, determine if sym == X, where X != V.
+  if (const llvm::APSInt* X = St.getSymVal(sym)) {
+    isFeasible = *X == V;
+    return St;
+  }
+  
+  // Second, determine if sym != V.
+  if (St.isNotEqual(sym, V)) {
+    isFeasible = false;
+    return St;
+  }
+  
+  // If we reach here, sym is not a constant and we don't know if it is == V.
+  // Make that assumption.
+  
+  isFeasible = true;
+  return StateMgr.AddEQ(St, sym, V);
+}
 
 //===----------------------------------------------------------------------===//
 // Driver.
diff --git a/Analysis/RValues.h b/Analysis/RValues.h
index 9c788ca..cd74262 100644
--- a/Analysis/RValues.h
+++ b/Analysis/RValues.h
@@ -149,6 +149,10 @@
   const llvm::APSInt& getValue(uint64_t X, QualType T,
                                SourceLocation Loc = SourceLocation());
   
+  inline const llvm::APSInt& getZeroWithPtrWidth() {
+    return getValue(0, Ctx.getTypeSize(Ctx.VoidPtrTy, SourceLocation()), true);
+  }
+  
   const SymIntConstraint& getConstraint(SymbolID sym, BinaryOperator::Opcode Op,
                                         const llvm::APSInt& V);
 };
diff --git a/Analysis/ValueState.cpp b/Analysis/ValueState.cpp
index aa6ddbd..418b06e 100644
--- a/Analysis/ValueState.cpp
+++ b/Analysis/ValueState.cpp
@@ -15,6 +15,24 @@
 
 using namespace clang;
 
+bool ValueState::isNotEqual(SymbolID sym, const llvm::APSInt& V) const {
+  // First, retrieve the NE-set associated with the given symbol.
+  ConstantNotEqTy::TreeTy* T = Data->ConstantNotEq.SlimFind(sym);
+  
+  if (!T)
+    return false;
+  
+  // Second, see if V is present in the NE-set.
+  return T->getValue().second.contains(&V);
+}
+
+const llvm::APSInt* ValueState::getSymVal(SymbolID sym) const {
+  ConstantEqTy::TreeTy* T = Data->ConstantEq.SlimFind(sym);
+  return T ? T->getValue().second : NULL;  
+}
+
+
+
 RValue ValueStateManager::GetValue(const StateTy& St, const LValue& LV) {
   switch (LV.getSubKind()) {
     case lval::DeclValKind: {
@@ -31,6 +49,36 @@
   return InvalidValue();
 }
 
+ValueStateManager::StateTy
+ValueStateManager::AddNE(StateTy St, SymbolID sym, const llvm::APSInt& V) {
+  // First, retrieve the NE-set associated with the given symbol.
+  ValueState::ConstantNotEqTy::TreeTy* T =
+    St.getImpl()->ConstantNotEq.SlimFind(sym);    
+  
+  ValueState::IntSetTy S = T ? T->getValue().second : ISetFactory.GetEmptySet();
+  
+  // Now add V to the NE set.  
+  S = ISetFactory.Add(S, &V);
+  
+  // Create a new state with the old binding replaced.
+  ValueStateImpl NewStateImpl = *St.getImpl();
+  NewStateImpl.ConstantNotEq = CNEFactory.Add(NewStateImpl.ConstantNotEq,
+                                              sym, S);
+    
+  // Get the persistent copy.
+  return getPersistentState(NewStateImpl);
+}
+
+ValueStateManager::StateTy
+ValueStateManager::AddEQ(StateTy St, SymbolID sym, const llvm::APSInt& V) {
+  // Create a new state with the old binding replaced.
+  ValueStateImpl NewStateImpl = *St.getImpl();
+  NewStateImpl.ConstantEq = CEFactory.Add(NewStateImpl.ConstantEq, sym, &V);
+  
+  // Get the persistent copy.
+  return getPersistentState(NewStateImpl);
+}
+
 RValue ValueStateManager::GetValue(const StateTy& St, Stmt* S, bool* hasVal) {
   for (;;) {
     switch (S->getStmtClass()) {
@@ -163,7 +211,8 @@
 
   // Create a state with empty variable bindings.
   ValueStateImpl StateImpl(VBFactory.GetEmptyMap(),
-                           CNEFactory.GetEmptyMap());
+                           CNEFactory.GetEmptyMap(),
+                           CEFactory.GetEmptyMap());
   
   return getPersistentState(StateImpl);
 }
diff --git a/Analysis/ValueState.h b/Analysis/ValueState.h
index 10abdce..b452979 100644
--- a/Analysis/ValueState.h
+++ b/Analysis/ValueState.h
@@ -116,8 +116,9 @@
 namespace vstate {
   typedef llvm::ImmutableSet<llvm::APSInt*> IntSetTy;
   
-  typedef llvm::ImmutableMap<VarBindKey,RValue> VariableBindingsTy;  
-  typedef llvm::ImmutableMap<SymbolID,IntSetTy> ConstantNotEqTy;
+  typedef llvm::ImmutableMap<VarBindKey,RValue>            VariableBindingsTy;  
+  typedef llvm::ImmutableMap<SymbolID,IntSetTy>            ConstantNotEqTy;
+  typedef llvm::ImmutableMap<SymbolID,const llvm::APSInt*> ConstantEqTy;
 }
 
 /// ValueStateImpl - This class encapsulates the actual data values for
@@ -127,22 +128,28 @@
 struct ValueStateImpl : public llvm::FoldingSetNode {
   vstate::VariableBindingsTy VariableBindings;
   vstate::ConstantNotEqTy    ConstantNotEq;
+  vstate::ConstantEqTy       ConstantEq;
   
   /// This ctor is used when creating the first ValueStateImpl object.
-  ValueStateImpl(vstate::VariableBindingsTy VB, vstate::ConstantNotEqTy CNE)
-    : VariableBindings(VB), ConstantNotEq(CNE) {}
+  ValueStateImpl(vstate::VariableBindingsTy VB,
+                 vstate::ConstantNotEqTy CNE,
+                 vstate::ConstantEqTy CE)
+    : VariableBindings(VB), ConstantNotEq(CNE), ConstantEq(CE) {}
   
   /// Copy ctor - We must explicitly define this or else the "Next" ptr
   ///  in FoldingSetNode will also get copied.
   ValueStateImpl(const ValueStateImpl& RHS)
     : llvm::FoldingSetNode(),
       VariableBindings(RHS.VariableBindings),
-      ConstantNotEq(RHS.ConstantNotEq) {} 
+      ConstantNotEq(RHS.ConstantNotEq),
+      ConstantEq(RHS.ConstantEq) {} 
   
   /// Profile - Profile the contents of a ValueStateImpl object for use
   ///  in a FoldingSet.
   static void Profile(llvm::FoldingSetNodeID& ID, const ValueStateImpl& V) {
     V.VariableBindings.Profile(ID);
+    V.ConstantNotEq.Profile(ID);
+    V.ConstantEq.Profile(ID);
   }
 
   /// Profile - Used to profile the contents of this object for inclusion
@@ -171,10 +178,18 @@
   ValueStateImpl* getImpl() const { return Data; }
 
   // Typedefs.
+  typedef vstate::IntSetTy                 IntSetTy;
   typedef vstate::VariableBindingsTy       VariableBindingsTy;
   typedef vstate::ConstantNotEqTy          ConstantNotEqTy;
+  typedef vstate::ConstantEqTy             ConstantEqTy;
+
   typedef llvm::SmallVector<ValueState,5>  BufferTy;
 
+  // Queries.
+  
+  bool isNotEqual(SymbolID sym, const llvm::APSInt& V) const;
+  const llvm::APSInt* getSymVal(SymbolID sym) const;
+  
   // Iterators.
 
   typedef VariableBindingsTy::iterator vb_iterator;  
@@ -211,8 +226,10 @@
   typedef ValueState StateTy;
 
 private:
+  ValueState::IntSetTy::Factory           ISetFactory;
   ValueState::VariableBindingsTy::Factory VBFactory;
   ValueState::ConstantNotEqTy::Factory    CNEFactory;
+  ValueState::ConstantEqTy::Factory       CEFactory;
   
   /// StateSet - FoldingSet containing all the states created for analyzing
   ///  a particular function.  This is used to unique states.
@@ -249,6 +266,9 @@
   StateTy Add(StateTy St, VarBindKey K, const RValue& V);
   StateTy Remove(StateTy St, VarBindKey K);
   StateTy getPersistentState(const ValueStateImpl& Impl);
+  
+  StateTy AddEQ(StateTy St, SymbolID sym, const llvm::APSInt& V);
+  StateTy AddNE(StateTy St, SymbolID sym, const llvm::APSInt& V);
 };
   
 } // end clang namespace