Change Solver::getValue to make explicit that result is a ConstantExpr.

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

1 files changed, 10 insertions, 4 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3db049cd..a673e9e7 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -110,14 +110,20 @@ bool Solver::mayBeFalse(const Query& query, bool &result) {
   return true;
 }
 
-bool Solver::getValue(const Query& query, ref<Expr> &result) {
+bool Solver::getValue(const Query& query, ref<ConstantExpr> &result) {
   // Maintain invariants implementation expect.
-  if (isa<ConstantExpr>(query.expr)) {
-    result = query.expr;
+  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
+    result = CE;
     return true;
   }
 
-  return impl->computeValue(query, result);
+  // FIXME: Push ConstantExpr requirement down.
+  ref<Expr> tmp;
+  if (!impl->computeValue(query, tmp))
+    return false;
+  
+  result = cast<ConstantExpr>(tmp);
+  return true;
 }
 
 bool