diff --git a/lib/Analysis/GRExprEngine.cpp b/lib/Analysis/GRExprEngine.cpp
index bc6a36c..e8c5be5 100644
--- a/lib/Analysis/GRExprEngine.cpp
+++ b/lib/Analysis/GRExprEngine.cpp
@@ -177,7 +177,7 @@
       if (T->isIntegerType())
         if (const MemRegion *R = StateMgr.getRegion(PD)) {
           SVal V = GetSVal(state, loc::MemRegionVal(R));
-          SVal Constraint = EvalBinOp(BinaryOperator::GT, V,
+          SVal Constraint = EvalBinOp(state, BinaryOperator::GT, V,
                                       ValMgr.makeZeroVal(T),
                                       getContext().IntTy);          
           bool isFeasible = false;          
@@ -841,7 +841,7 @@
         
     do {
       nonloc::ConcreteInt CaseVal(getBasicVals().getValue(V1.Val.getInt()));      
-      SVal Res = EvalBinOp(BinaryOperator::EQ, CondV, CaseVal,
+      SVal Res = EvalBinOp(DefaultSt, BinaryOperator::EQ, CondV, CaseVal,
                            getContext().IntTy);
       
       // Now "assume" that the case matches.      
@@ -1333,7 +1333,8 @@
     SVal oldValueVal = StateMgr.GetSVal(stateLoad, oldValueExpr);
         
     // Perform the comparison.
-    SVal Cmp = Engine.EvalBinOp(BinaryOperator::EQ, theValueVal, oldValueVal,
+    SVal Cmp = Engine.EvalBinOp(stateLoad,
+                                BinaryOperator::EQ, theValueVal, oldValueVal,
                                 Engine.getContext().IntTy);
     bool isFeasible = false;
     const GRState *stateEqual = StateMgr.Assume(stateLoad, Cmp, true,
@@ -2622,7 +2623,7 @@
             
             if (isa<Loc>(V)) {
               Loc X = Loc::MakeNull(getBasicVals());
-              SVal Result = EvalBinOp(BinaryOperator::EQ, cast<Loc>(V), X,
+              SVal Result = EvalBinOp(state,BinaryOperator::EQ, cast<Loc>(V), X,
                                       U->getType());
               state = BindExpr(state, U, Result);
             }
@@ -2679,7 +2680,8 @@
       BinaryOperator::Opcode Op = U->isIncrementOp() ? BinaryOperator::Add
                                                      : BinaryOperator::Sub;
 
-      SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U), U->getType());    
+      SVal Result = EvalBinOp(state, Op, V2, MakeConstantVal(1U, U), 
+                              U->getType());    
       
       // Conjure a new symbol if necessary to recover precision.
       if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result)){
@@ -2690,7 +2692,7 @@
         // non-nullness.  Check if the original value was non-null, and if so propagate
         // that constraint.        
         if (Loc::IsLocType(U->getType())) {
-          SVal Constraint = EvalBinOp(BinaryOperator::EQ, V2,
+          SVal Constraint = EvalBinOp(state, BinaryOperator::EQ, V2,
                                       ValMgr.makeZeroVal(U->getType()),
                                       getContext().IntTy);          
           
@@ -2699,7 +2701,7 @@
           if (!isFeasible) {
             // It isn't feasible for the original value to be null.
             // Propagate this constraint.
-            Constraint = EvalBinOp(BinaryOperator::EQ, Result,
+            Constraint = EvalBinOp(state, BinaryOperator::EQ, Result,
                                    ValMgr.makeZeroVal(U->getType()),
                                    getContext().IntTy);
             
@@ -2965,7 +2967,7 @@
           // Process non-assignements except commas or short-circuited
           // logical expressions (LAnd and LOr).
           
-          SVal Result = EvalBinOp(Op, LeftV, RightV, B->getType());
+          SVal Result = EvalBinOp(state, Op, LeftV, RightV, B->getType());
           
           if (Result.isUnknown()) {
             if (OldSt != state) {
@@ -3079,7 +3081,8 @@
         }
       
         // Compute the result of the operation.      
-        SVal Result = EvalCast(EvalBinOp(Op, V, RightV, CTy), B->getType());
+        SVal Result = EvalCast(EvalBinOp(state, Op, V, RightV, CTy), 
+                               B->getType());
           
         if (Result.isUndef()) {
           // The operands were not undefined, but the result is undefined.
@@ -3147,8 +3150,8 @@
   if (R.isValid()) getTF().EvalBinOpNN(OStates, *this, state, Ex, Op, L, R, T);
 }
 
-SVal GRExprEngine::EvalBinOp(BinaryOperator::Opcode Op, SVal L, SVal R,
-                             QualType T) {
+SVal GRExprEngine::EvalBinOp(const GRState* state, BinaryOperator::Opcode Op, 
+                             SVal L, SVal R, QualType T) {
   
   if (L.isUndef() || R.isUndef())
     return UndefinedVal();
@@ -3160,7 +3163,7 @@
     if (isa<Loc>(R))
       return getTF().EvalBinOp(*this, Op, cast<Loc>(L), cast<Loc>(R));
     else
-      return getTF().EvalBinOp(*this, Op, cast<Loc>(L), cast<NonLoc>(R));
+      return getTF().EvalBinOp(*this, state, Op, cast<Loc>(L), cast<NonLoc>(R));
   }
   
   if (isa<Loc>(R)) {
@@ -3170,8 +3173,7 @@
     assert (Op == BinaryOperator::Add || Op == BinaryOperator::Sub);
     
     // Commute the operands.
-    return getTF().EvalBinOp(*this, Op, cast<Loc>(R),
-                             cast<NonLoc>(L));
+    return getTF().EvalBinOp(*this, state, Op, cast<Loc>(R), cast<NonLoc>(L));
   }
   else
     return getTF().DetermEvalBinOpNN(*this, Op, cast<NonLoc>(L),
diff --git a/lib/Analysis/GRSimpleVals.cpp b/lib/Analysis/GRSimpleVals.cpp
index 17e3c38..e1c4848 100644
--- a/lib/Analysis/GRSimpleVals.cpp
+++ b/lib/Analysis/GRSimpleVals.cpp
@@ -257,8 +257,8 @@
   }
 }
 
-SVal GRSimpleVals::EvalBinOp(GRExprEngine& Eng, BinaryOperator::Opcode Op,
-                             Loc L, NonLoc R) {
+SVal GRSimpleVals::EvalBinOp(GRExprEngine& Eng, const GRState *state, 
+                             BinaryOperator::Opcode Op, Loc L, NonLoc R) {
   
   // Special case: 'R' is an integer that has the same width as a pointer and
   // we are using the integer location in a comparison.  Normally this cannot be
@@ -280,7 +280,7 @@
   }
   
   // Delegate pointer arithmetic to store manager.
-  return Eng.getStoreManager().EvalBinOp(Op, L, R);
+  return Eng.getStoreManager().EvalBinOp(state, Op, L, R);
 }
 
 // Equality operators for Locs.  
diff --git a/lib/Analysis/GRSimpleVals.h b/lib/Analysis/GRSimpleVals.h
index 1258cbc..6ef49dc 100644
--- a/lib/Analysis/GRSimpleVals.h
+++ b/lib/Analysis/GRSimpleVals.h
@@ -53,8 +53,8 @@
   
   // Pointer arithmetic.
   
-  virtual SVal EvalBinOp(GRExprEngine& Engine, BinaryOperator::Opcode Op,
-                         Loc L, NonLoc R);  
+  virtual SVal EvalBinOp(GRExprEngine& Engine, const GRState *state,
+                         BinaryOperator::Opcode Op, Loc L, NonLoc R);  
   
   // Calls.
   
diff --git a/lib/Analysis/RegionStore.cpp b/lib/Analysis/RegionStore.cpp
index e1d875b..be34bd5 100644
--- a/lib/Analysis/RegionStore.cpp
+++ b/lib/Analysis/RegionStore.cpp
@@ -214,7 +214,7 @@
   CastResult CastRegion(const GRState* state, const MemRegion* R,
                         QualType CastToTy);
 
-  SVal EvalBinOp(BinaryOperator::Opcode Op, Loc L, NonLoc R);
+  SVal EvalBinOp(const GRState *state,BinaryOperator::Opcode Op,Loc L,NonLoc R);
 
   /// The high level logic for this method is this:
   /// Retrieve (L)
@@ -636,15 +636,17 @@
   return 0;
 }
 
-SVal RegionStoreManager::EvalBinOp(BinaryOperator::Opcode Op, Loc L, NonLoc R) {
+SVal RegionStoreManager::EvalBinOp(const GRState *state, 
+                                   BinaryOperator::Opcode Op, Loc L, NonLoc R) {
   // Assume the base location is MemRegionVal.
   if (!isa<loc::MemRegionVal>(L))
     return UnknownVal();
 
   const MemRegion* MR = cast<loc::MemRegionVal>(L).getRegion();
   const ElementRegion *ER = 0;
-  // If the operand is a symbolic region, we convert it to the first element
-  // region implicitly.
+
+  // If the operand is a symbolic or alloca region, create the first element
+  // region on it.
   if (const SymbolicRegion *SR = dyn_cast<SymbolicRegion>(MR)) {
     // Get symbol's type. It should be a pointer type.
     SymbolRef Sym = SR->getSymbol();
@@ -653,7 +655,18 @@
 
     SVal ZeroIdx = ValMgr.makeZeroArrayIndex();
     ER = MRMgr.getElementRegion(EleTy, ZeroIdx, SR);
-  } else
+  } 
+  else if (const AllocaRegion *AR = dyn_cast<AllocaRegion>(MR)) {
+    // Get the alloca region's current cast type.
+    GRStateRef StRef(state, StateMgr);
+
+    GRStateTrait<RegionCasts>::lookup_type T = StRef.get<RegionCasts>(AR);
+    assert(T && "alloca region has no type.");
+    QualType EleTy = cast<PointerType>(T->getTypePtr())->getPointeeType();
+    SVal ZeroIdx = ValMgr.makeZeroArrayIndex();
+    ER = MRMgr.getElementRegion(EleTy, ZeroIdx, AR);
+  } 
+  else
     ER = cast<ElementRegion>(MR);
 
   SVal Idx = ER->getIndex();