From 21fb3bd80309b30ed2223e793003ac4744776dfb Mon Sep 17 00:00:00 2001 From: Daniel Dunbar 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 &result) { +bool Solver::getValue(const Query& query, ref &result) { // Maintain invariants implementation expect. - if (isa(query.expr)) { - result = query.expr; + if (ConstantExpr *CE = dyn_cast(query.expr)) { + result = CE; return true; } - return impl->computeValue(query, result); + // FIXME: Push ConstantExpr requirement down. + ref tmp; + if (!impl->computeValue(query, tmp)) + return false; + + result = cast(tmp); + return true; } bool -- cgit 1.4.1