3 files changed, 10 insertions, 11 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 9c233530..373f42d9 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -139,7 +139,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
-    if (!CE->getConstantValue()) {
+    if (CE->isFalse()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -154,7 +154,7 @@ bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(neg)) {
-    if (!CE->getConstantValue()) {
+    if (CE->isFalse()) {
       result = (Assignment*) 0;
       return true;
     }
@@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   assert(isa<ConstantExpr>(q) && 
          "assignment evaluation did not result in constant");
 
-  if (cast<ConstantExpr>(q)->getConstantValue()) {
+  if (cast<ConstantExpr>(q)->isTrue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index ab65f254..8680d0a8 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -608,11 +608,10 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
     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
-	  return constructSDivByConstant( left, *width_out, divisor);
+	  return constructSDivByConstant( left, *width_out, 
+                                          CE->getConstantValue());
       }
     } 
 
@@ -776,9 +775,9 @@ 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 (isa<ConstantExpr>(ee->left)) {
-        assert(!cast<ConstantExpr>(ee->left)->getConstantValue() && 
-               "uncanonicalized eq");
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        if (CE->isTrue())
+          return right;
         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 7a1b356c..9e8e37bf 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -57,7 +57,7 @@ bool Solver::evaluate(const Query& query, Validity &result) {
 
   // Maintain invariants implementations expect.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
-    result = CE->getConstantValue() ? True : False;
+    result = CE->isTrue() ? True : False;
     return true;
   }
 
@@ -83,7 +83,7 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
 
   // Maintain invariants implementations expect.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
-    result = CE->getConstantValue() ? true : false;
+    result = CE->isTrue() ? true : false;
     return true;
   }