about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CexCachingSolver.cpp2
-rw-r--r--lib/Solver/FastCexSolver.cpp7
-rw-r--r--lib/Solver/STPBuilder.cpp2
3 files changed, 5 insertions, 6 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 1eaec4d9..9c233530 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -220,7 +220,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
   assert(isa<ConstantExpr>(q) && 
          "assignment evaluation did not result in constant");
 
-  if (q->getConstantValue()) {
+  if (cast<ConstantExpr>(q)->getConstantValue()) {
     if (!getAssignment(query, a))
       return false;
     result = !a ? Solver::True : Solver::Unknown;
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 1a1cfe62..6d9c8551 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -730,10 +730,9 @@ public:
   bool exprMustBeValue(ref<Expr> e, uint64_t value) {
     CexConstifier cc(objectValues);
     ref<Expr> v = cc.visit(e);
-    if (!isa<ConstantExpr>(v)) return false;
-    // XXX reenable once all reads and vars are fixed
-    //    assert(v.isConstant() && "not all values have been fixed");
-    return v->getConstantValue() == value;
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(v))
+      return CE->getConstantValue() == value;
+    return false;
   }
 };
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 88bdd2b0..5b3fdd60 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -449,7 +449,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
 
   switch (e->getKind()) {
   case Expr::Constant: {
-    uint64_t asUInt64 = e->getConstantValue();
+    uint64_t asUInt64 = cast<ConstantExpr>(e)->getConstantValue();
     *width_out = e->getWidth();
 
     if (*width_out > 64)