From 21fb3bd80309b30ed2223e793003ac4744776dfb Mon Sep 17 00:00:00 2001
From: Daniel Dunbar <daniel@zuster.org>
Date: Thu, 4 Jun 2009 08:42:34 +0000
Subject: 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
---
 lib/Solver/Solver.cpp | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'lib/Solver')

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 
-- 
cgit 1.4.1