Finish removing uses of Expr::isConstant.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72859 91177308-0d34-0410-b5e6-96231b3b80d8

13 files changed, 135 insertions, 135 deletions

diff --git a/include/klee/Expr.h b/include/klee/Expr.h
index 3473784b..2945b697 100644
--- a/include/klee/Expr.h
+++ b/include/klee/Expr.h
@@ -197,7 +197,6 @@ public:
 
   ///
 
-  bool isConstant() const { return getKind() == Expr::Constant; }
   uint64_t getConstantValue() const;
 
   /* Static utility methods */
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index dfb91344..b8d44eea 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -53,13 +53,13 @@ static void _getImpliedValue(ref<Expr> e,
     // not much to do, could improve with range analysis
     SelectExpr *se = cast<SelectExpr>(e);
     
-    if (se->trueExpr->isConstant()) {
-      if (se->falseExpr->isConstant()) {
-        if (se->trueExpr->getConstantValue() != se->falseExpr->getConstantValue()) {
-          if (value == se->trueExpr->getConstantValue()) {
+    if (ConstantExpr *TrueCE = dyn_cast<ConstantExpr>(se->trueExpr)) {
+      if (ConstantExpr *FalseCE = dyn_cast<ConstantExpr>(se->falseExpr)) {
+        if (TrueCE->getConstantValue() != FalseCE->getConstantValue()) {
+          if (value == TrueCE->getConstantValue()) {
             _getImpliedValue(se->cond, 1, results);
           } else {
-            assert(value == se->falseExpr->getConstantValue() &&
+            assert(value == FalseCE->getConstantValue() &&
                    "err in implied value calculation");
             _getImpliedValue(se->cond, 0, results);
           }
@@ -97,20 +97,20 @@ static void _getImpliedValue(ref<Expr> e,
 
   case Expr::Add: { // constants on left
     BinaryExpr *be = cast<BinaryExpr>(e);
-    if (be->left->isConstant()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
       uint64_t nvalue = ints::sub(value,
-                                  be->left->getConstantValue(),
-                                  be->left->getWidth());
+                                  CE->getConstantValue(),
+                                  CE->getWidth());
       _getImpliedValue(be->right, nvalue, results);
     }
     break;
   }
   case Expr::Sub: { // constants on left
     BinaryExpr *be = cast<BinaryExpr>(e);
-    if (be->left->isConstant()) {
-      uint64_t nvalue = ints::sub(be->left->getConstantValue(),
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
+      uint64_t nvalue = ints::sub(CE->getConstantValue(),
                                   value,
-                                  be->left->getWidth());
+                                  CE->getWidth());
       _getImpliedValue(be->right, nvalue, results);
     }
     break;
@@ -156,8 +156,8 @@ static void _getImpliedValue(ref<Expr> e,
   }
   case Expr::Xor: { // constants on left
     BinaryExpr *be = cast<BinaryExpr>(e);
-    if (be->left->isConstant()) {
-      _getImpliedValue(be->right, value ^ be->left->getConstantValue(), results);
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
+      _getImpliedValue(be->right, value ^ CE->getConstantValue(), results);
     }
     break;
   }
@@ -169,8 +169,8 @@ static void _getImpliedValue(ref<Expr> e,
   case Expr::Eq: {
     EqExpr *ee = cast<EqExpr>(e);
     if (value) {
-      if (ee->left->isConstant())
-        _getImpliedValue(ee->right, ee->left->getConstantValue(), results);
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left))
+        _getImpliedValue(ee->right, CE->getConstantValue(), results);
     } else {
       // look for limited value range, woohoo
       //
@@ -180,9 +180,9 @@ static void _getImpliedValue(ref<Expr> e,
       // expression where the true and false branches are single
       // valued and distinct.
       
-      if (ee->left->isConstant()) {
-        if (ee->left->getWidth() == Expr::Bool) {
-          _getImpliedValue(ee->right, !ee->left->getConstantValue(), results);
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        if (CE->getWidth() == Expr::Bool) {
+          _getImpliedValue(ee->right, !CE->getConstantValue(), results);
         }
       }
     }
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index b4c433b1..5a3af34c 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -301,7 +301,7 @@ ref<Expr> ObjectState::read8(unsigned offset) const {
 }
 
 ref<Expr> ObjectState::read8(ref<Expr> offset) const {
-  assert(!offset->isConstant() && "constant offset passed to symbolic read8");
+  assert(!isa<ConstantExpr>(offset) && "constant offset passed to symbolic read8");
   unsigned base, size;
   fastRangeCheckOffset(offset, &base, &size);
   flushRangeForRead(base, size);
@@ -328,8 +328,8 @@ void ObjectState::write8(unsigned offset, uint8_t value) {
 
 void ObjectState::write8(unsigned offset, ref<Expr> value) {
   // can happen when ExtractExpr special cases
-  if (value->isConstant()) {
-    write8(offset, (uint8_t) value->getConstantValue());
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
+    write8(offset, (uint8_t) CE->getConstantValue());
   } else {
     setKnownSymbolic(offset, value.get());
       
@@ -358,8 +358,8 @@ void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
 /***/
 
 ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
-  if (offset->isConstant()) {
-    return read((unsigned) offset->getConstantValue(), width);
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) {
+    return read((unsigned) CE->getConstantValue(), width);
   } else { 
     switch (width) {
     case  Expr::Bool: return  read1(offset);
@@ -547,8 +547,8 @@ ref<Expr> ObjectState::read64(ref<Expr> offset) const {
 
 void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
-  if (offset->isConstant()) {
-    write(offset->getConstantValue(), value);
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(offset)) {
+    write(CE->getConstantValue(), value);
   } else {
     switch(w) {
     case  Expr::Bool:  write1(offset, value); break;
@@ -563,8 +563,8 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
 
 void ObjectState::write(unsigned offset, ref<Expr> value) {
   Expr::Width w = value->getWidth();
-  if (value->isConstant()) {
-    uint64_t val = value->getConstantValue();
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
+    uint64_t val = CE->getConstantValue();
     switch(w) {
     case  Expr::Bool:
     case  Expr::Int8:  write8(offset, val); break;
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index e1182cf0..0ec9a5ac 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -376,7 +376,8 @@ void SpecialFunctionHandler::handleIsSymbolic(ExecutionState &state,
   assert(arguments.size()==1 && "invalid number of arguments to klee_is_symbolic");
 
   executor.bindLocal(target, state, 
-                     ConstantExpr::create(!arguments[0]->isConstant(), Expr::Int32));
+                     ConstantExpr::create(!isa<ConstantExpr>(arguments[0]),
+                                          Expr::Int32));
 }
 
 void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
@@ -415,7 +416,7 @@ void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
   // XXX should type check args
   assert(arguments.size()==1 &&
          "invalid number of arguments to klee_under_constrained().");
-  assert(arguments[0]->isConstant() &&
+  assert(isa<ConstantExpr>(arguments[0]) &&
    	 "symbolic argument given to klee_under_constrained!");
 
   unsigned v = arguments[0]->getConstantValue();
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 9efb77b8..b26551cc 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -25,8 +25,8 @@ using namespace llvm;
 bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
                             Solver::Validity &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr->isConstant()) {
-    result = expr->getConstantValue() ? Solver::True : Solver::False;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
+    result = CE->getConstantValue() ? Solver::True : Solver::False;
     return true;
   }
 
@@ -49,8 +49,8 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
 bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, 
                               bool &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr->isConstant()) {
-    result = expr->getConstantValue() ? true : false;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
+    result = CE->getConstantValue() ? true : false;
     return true;
   }
 
@@ -96,7 +96,7 @@ bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr,
 bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, 
                             ref<Expr> &result) {
   // Fast path, to avoid timer and OS overhead.
-  if (expr->isConstant()) {
+  if (isa<ConstantExpr>(expr)) {
     result = expr;
     return true;
   }
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 9103c7c3..5869a852 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -87,7 +87,7 @@ void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
 }
 
 ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
-  if (e->isConstant())
+  if (isa<ConstantExpr>(e))
     return e;
 
   std::map< ref<Expr>, ref<Expr> > equalities;
@@ -95,7 +95,7 @@ ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
   for (ConstraintManager::constraints_ty::const_iterator 
          it = constraints.begin(), ie = constraints.end(); it != ie; ++it) {
     if (const EqExpr *ee = dyn_cast<EqExpr>(*it)) {
-      if (ee->left->isConstant()) {
+      if (isa<ConstantExpr>(ee->left)) {
         equalities.insert(std::make_pair(ee->right,
                                          ee->left));
       } else {
@@ -135,7 +135,7 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 
   case Expr::Eq: {
     BinaryExpr *be = cast<BinaryExpr>(e);
-    if (be->left->isConstant()) {
+    if (isa<ConstantExpr>(be->left)) {
       ExprReplaceVisitor visitor(be->right, be->left);
       rewriteConstraints(visitor);
     }
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 0a174179..f95369f4 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -378,8 +378,8 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
   for (; un; un=un->next) {
     ref<Expr> cond = EqExpr::create(index, un->index);
     
-    if (cond->isConstant()) {
-      if (cond->getConstantValue())
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
+      if (CE->getConstantValue())
         return un->value;
     } else {
       break;
@@ -399,19 +399,19 @@ ref<Expr> SelectExpr::create(ref<Expr> c, ref<Expr> t, ref<Expr> f) {
   assert(c->getWidth()==Bool && "type mismatch");
   assert(kt==f->getWidth() && "type mismatch");
 
-  if (c->isConstant()) {
-    return c->getConstantValue() ? t : f;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(c)) {
+    return CE->getConstantValue() ? t : f;
   } else if (t==f) {
     return t;
   } else if (kt==Expr::Bool) { // c ? t : f  <=> (c and t) or (not c and f)
-    if (t->isConstant()) {      
-      if (t->getConstantValue()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(t)) {      
+      if (CE->getConstantValue()) {
         return OrExpr::create(c, f);
       } else {
         return AndExpr::create(Expr::createNot(c), f);
       }
-    } else if (f->isConstant()) {
-      if (f->getConstantValue()) {
+    } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(f)) {
+      if (CE->getConstantValue()) {
         return OrExpr::create(Expr::createNot(c), t);
       } else {
         return AndExpr::create(c, t);
@@ -483,12 +483,12 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
   unsigned kw = expr->getWidth();
   assert(w > 0 && off + w <= kw && "invalid extract");
   
-  if (w == kw)
+  if (w == kw) {
     return expr;
-  else if (expr->isConstant()) {
-    return ConstantExpr::create(ints::trunc(expr->getConstantValue() >> off, w, kw), w);
-  } 
-  else 
+  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
+    return ConstantExpr::create(ints::trunc(CE->getConstantValue() >> off, w, 
+                                            kw), w);
+  } else {
     // Extract(Concat)
     if (ConcatExpr *ce = dyn_cast<ConcatExpr>(expr)) {
       // if the extract skips the right side of the concat
@@ -503,6 +503,7 @@ ref<Expr> ExtractExpr::create(ref<Expr> expr, unsigned off, Width w) {
       return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1)->getWidth() + off),
 				ExtractExpr::create(ce->getKid(1), off, ce->getKid(1)->getWidth() - off));
     }
+  }
   
   return ExtractExpr::alloc(expr, off, w);
 }
@@ -521,10 +522,9 @@ ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
-    if (e->isConstant()) {
-      return ConstantExpr::create(ints::zext(e->getConstantValue(), w, kBits),
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+      return ConstantExpr::create(ints::zext(CE->getConstantValue(), w, kBits),
                                   w);
-    }
     
     return ZExtExpr::alloc(e, w);
   }
@@ -537,10 +537,9 @@ ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
   } else if (w < kBits) { // trunc
     return ExtractExpr::createByteOff(e, 0, w);
   } else {
-    if (e->isConstant()) {
-      return ConstantExpr::create(ints::sext(e->getConstantValue(), w, kBits),
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
+      return ConstantExpr::create(ints::sext(CE->getConstantValue(), w, kBits),
                                   w);
-    }
     
     return SExtExpr::alloc(e, w);
   }
@@ -612,10 +611,10 @@ static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     return XorExpr_createPartialR(cl, r);
   } else {
     Expr::Kind rk = r->getKind();
-    if (rk==Expr::Add && r->getKid(0)->isConstant()) { // A - (B+c) == (A-B) - c
+    if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // A - (B+c) == (A-B) - c
       return SubExpr::create(SubExpr::create(cl, r->getKid(0)),
                              r->getKid(1));
-    } else if (rk==Expr::Sub && r->getKid(0)->isConstant()) { // A - (B-c) == (A-B) + c
+    } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // A - (B-c) == (A-B) + c
       return AddExpr::create(SubExpr::create(cl, r->getKid(0)),
                              r->getKid(1));
     } else {
@@ -624,7 +623,6 @@ static ref<Expr> SubExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
   }
 }
 static ref<Expr> SubExpr_createPartial(Expr *l, const ref<ConstantExpr> &cr) {
-  assert(cr->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cr->getConstantValue();
   Expr::Width width = cr->getWidth();
   uint64_t nvalue = ints::sub(0, value, width);
@@ -659,7 +657,6 @@ static ref<Expr> SubExpr_create(Expr *l, Expr *r) {
 }
 
 static ref<Expr> MulExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
-  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width type = cl->getWidth();
 
@@ -897,9 +894,8 @@ static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
 /// rd a ReadExpr.  If rd is a read into an all-constant array,
 /// returns a disjunction of equalities on the index.  Otherwise,
 /// returns the initial equality expression. 
-static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl, 
+static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl, 
 				  ReadExpr *rd) {
-  assert(cl->isConstant() && "constant expression required");
   assert(rd->getKind() == Expr::Read && "read expression required");
   
   uint64_t ct = cl->getConstantValue();
@@ -921,22 +917,21 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 
       ref<Expr> idx = un->index;
       ref<Expr> val = un->value;
-      if (!idx->isConstant() || !val->isConstant()) {
-	all_const = false;
-	//llvm::cerr << "Idx or val not constant\n";
-	break;
+      ConstantExpr *idxCE = dyn_cast<ConstantExpr>(idx);
+      ConstantExpr *valCE = dyn_cast<ConstantExpr>(val);
+      if (!idxCE || !valCE) {
+        all_const = false;
+        break;
+      }
+
+      if (idxCE->getConstantValue() != k) {
+        all_const = false;
+        break;
       }
-      else {
-	if (idx->getConstantValue() != k) {
-	  all_const = false;
-	  //llvm::cerr << "Wrong constant\n";
-	  break;
-	}
-	if (val->getConstantValue() == ct) {
-	  matches++;
-	  if (matches == 1)
-	    first_idx_match = un->index;
-	}
+      if (valCE->getConstantValue() == ct) {
+        matches++;
+        if (matches == 1)
+          first_idx_match = un->index;
       }
     }
   }
@@ -968,7 +963,6 @@ static ref<Expr> TryConstArrayOpt(const ref<Expr> &cl,
 
 
 static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {  
-  assert(cl->isConstant() && "non-constant passed in place of constant");
   uint64_t value = cl->getConstantValue();
   Expr::Width width = cl->getWidth();
 
@@ -983,10 +977,11 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
         const EqExpr *ree = cast<EqExpr>(r);
 
         // eliminate double negation
-        if (ree->left->isConstant() &&
-            ree->left->getWidth()==Expr::Bool) {
-          assert(!ree->left->getConstantValue());
-          return ree->right;
+        if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ree->left)) {
+          if (CE->getWidth() == Expr::Bool) {
+            assert(!CE->getConstantValue());
+            return ree->right;
+          }
         }
       } else if (rk == Expr::Or) {
         const OrExpr *roe = cast<OrExpr>(r);
@@ -1024,7 +1019,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     }
   } else if (rk==Expr::Add) {
     const AddExpr *ae = cast<AddExpr>(r);
-    if (ae->left->isConstant()) {
+    if (isa<ConstantExpr>(ae->left)) {
       // c0 = c1 + b => c0 - c1 = b
       return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(cl, 
                                                                       ae->left)),
@@ -1032,7 +1027,7 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) {
     }
   } else if (rk==Expr::Sub) {
     const SubExpr *se = cast<SubExpr>(r);
-    if (se->left->isConstant()) {
+    if (isa<ConstantExpr>(se->left)) {
       // c0 = c1 - b => c1 - c0 = b
       return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(se->left, 
                                                                       cl)),
@@ -1073,8 +1068,8 @@ static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
   if (t == Expr::Bool) { // !l && r
     return AndExpr::create(Expr::createNot(l), r);
   } else {
-    if (r->isConstant()) {      
-      uint64_t value = r->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(r)) {      
+      uint64_t value = CE->getConstantValue();
       if (value <= 8) {
         ref<Expr> res = ConstantExpr::alloc(0, Expr::Bool);
         for (unsigned i=0; i<value; i++) {
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index 038fe8b8..ca8f1611 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -16,8 +16,8 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
   for (const UpdateNode *un=ul.head; un; un=un->next) {
     ref<Expr> ui = visit(un->index);
     
-    if (ui->isConstant()) {
-      if (ui->getConstantValue() == index)
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
+      if (CE->getConstantValue() == index)
         return Action::changeTo(visit(un->value));
     } else {
       // update index is unknown, so may or may not be index, we
@@ -36,8 +36,8 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
 ExprVisitor::Action ExprEvaluator::visitRead(const ReadExpr &re) {
   ref<Expr> v = visit(re.index);
   
-  if (v->isConstant()) {
-    return evalRead(re.updates, v->getConstantValue());
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v)) {
+    return evalRead(re.updates, CE->getConstantValue());
   } else {
     return Action::doChildren();
   }
@@ -50,8 +50,9 @@ ExprVisitor::Action ExprEvaluator::protectedDivOperation(const BinaryExpr &e) {
   ref<Expr> kids[2] = { visit(e.left),
                         visit(e.right) };
 
-  if (kids[1]->isConstant() && !kids[1]->getConstantValue())
-    kids[1] = e.right;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(kids[1]))
+    if (!CE->getConstantValue())
+      kids[1] = e.right;
 
   if (kids[0]!=e.left || kids[1]!=e.right) {
     return Action::changeTo(e.rebuild(kids));
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 49db74e8..1eaec4d9 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -138,8 +138,8 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
                                         Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg->isConstant()) {
-    if (!neg->getConstantValue()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
+    if (!CE->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -153,8 +153,8 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg->isConstant()) {
-    if (!neg->getConstantValue()) {
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
+    if (!CE->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
     }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index a0d943d3..1a1cfe62 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -416,16 +416,17 @@ public:
 
       // XXX we need to respect the version here and object state chain
 
-      if (re->index->isConstant() && 
-          re->index->getConstantValue() < array->size) {
-        CexValueData &cvd = cod.values[re->index->getConstantValue()];
-        CexValueData tmp = cvd.set_intersection(range);
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
+        if (CE->getConstantValue() < array->size) {
+          CexValueData &cvd = cod.values[CE->getConstantValue()];
+          CexValueData tmp = cvd.set_intersection(range);
         
-        if (tmp.isEmpty()) {
-          if (range.isFixed()) // ranges conflict, if new one is fixed use that
-            cvd = range;
-        } else {
-          cvd = tmp;
+          if (tmp.isEmpty()) {
+            if (range.isFixed()) // ranges conflict, if new one is fixed use that
+              cvd = range;
+          } else {
+            cvd = tmp;
+          }
         }
       } else {
         // XXX        fatal("XXX not implemented");
@@ -613,8 +614,8 @@ public:
     case Expr::Eq: {
       BinaryExpr *be = cast<BinaryExpr>(e);
       if (range.isFixed()) {
-        if (be->left->isConstant()) {
-          uint64_t value = be->left->getConstantValue();
+        if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
+          uint64_t value = CE->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
           } else {
@@ -939,8 +940,8 @@ FastCexSolver::computeInitialValues(const Query& query,
                                   ConstantExpr::create(i,
                                                        kMachinePointerType)));
       
-      if (value->isConstant()) {
-        data.push_back(value->getConstantValue());
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
+        data.push_back(CE->getConstantValue());
       } else {
         // FIXME: When does this happen?
         return false;
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 4e004fd8..455e9240 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -97,9 +97,9 @@ public:
       if (re->updates.isRooted) {
         const Array *array = re->updates.root;
         if (!wholeObjects.count(array)) {
-          if (re->index->isConstant()) {
+          if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
             DenseSet<unsigned> &dis = elements[array];
-            dis.add((unsigned) re->index->getConstantValue());
+            dis.add((unsigned) CE->getConstantValue());
           } else {
             elements_ty::iterator it2 = elements.find(array);
             if (it2!=elements.end())
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 00fd8e4a..88bdd2b0 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -555,9 +555,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (me->left->isConstant()) {
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left)) {
       return constructMulByConstant(right, *width_out, 
-                                    me->left->getConstantValue());
+                                    CE->getConstantValue());
     } else {
       ExprHandle left = construct(me->left, width_out);
       return vc_bvMultExpr(vc, *width_out, left, right);
@@ -569,8 +569,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized udiv");
     
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      uint64_t divisor = CE->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
         return bvRightShift(left,
@@ -591,8 +591,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      uint64_t divisor = CE->getConstantValue();
  
       if (optimizeDivides) {
 	if (*width_out == 32) //only works for 32-bit division
@@ -611,8 +611,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized urem");
     
-    if (de->right->isConstant()) {
-      uint64_t divisor = de->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      uint64_t divisor = CE->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
         unsigned bits = bits64::indexOfSingleBit(divisor);
@@ -710,8 +710,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(se->left, width_out);
     assert(*width_out!=1 && "uncanonicalized shl");
 
-    if (se->right->isConstant()) {
-      return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
+      return bvLeftShift(left, CE->getConstantValue(), 
+                         getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(se->right, &shiftWidth);
@@ -725,8 +726,9 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
-    if (lse->right->isConstant()) {
-      return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
+      return bvRightShift(left, (unsigned) CE->getConstantValue(), 
+                          shiftBits);
     } else {
       int shiftWidth;
       ExprHandle amount = construct(lse->right, &shiftWidth);
@@ -739,10 +741,11 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ase->left, width_out);
     assert(*width_out!=1 && "uncanonicalized ashr");
     
-    if (ase->right->isConstant()) {
-      unsigned shift = (unsigned) ase->right->getConstantValue();
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+      unsigned shift = (unsigned) CE->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
-      return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
+      return constructAShrByConstant(left, shift, signedBool, 
+                                     getShiftBits(*width_out));
     } else {
       int shiftWidth;
       ExprHandle amount = construct(ase->right, &shiftWidth);
@@ -757,8 +760,8 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ee->left, width_out);
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
-      if (ee->left->isConstant()) {
-        assert(!ee->left->getConstantValue() && "uncanonicalized eq");
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        assert(!CE->getConstantValue() && "uncanonicalized eq");
         return vc_notExpr(vc, right);
       } else {
         return vc_iffExpr(vc, left, right);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 6cbf6ac0..3db049cd 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -56,8 +56,8 @@ bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr->isConstant()) {
-    result = query.expr->getConstantValue() ? True : False;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE->getConstantValue() ? True : False;
     return true;
   }
 
@@ -82,8 +82,8 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr->isConstant()) {
-    result = query.expr->getConstantValue() ? true : false;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE->getConstantValue() ? true : false;
     return true;
   }
 
@@ -151,8 +151,8 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
     default:
       min = 0, max = 1; break;
     }
-  } else if (e->isConstant()) {
-    min = max = e->getConstantValue();
+  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
+    min = max = CE->getConstantValue();
   } else {
     // binary search for # of useful bits
     uint64_t lo=0, hi=width, mid, bits=0;