diff options
Diffstat (limited to 'lib/Solver/Solver.cpp')
| -rw-r--r-- | lib/Solver/Solver.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 22b1545f..229fa234 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -407,11 +407,12 @@ ValidatingSolver::computeInitialValues(const Query& query, std::vector< ref<Expr> > bindings; for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; + assert(array); for (unsigned j=0; j<array->size; j++) { unsigned char value = values[i][j]; bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(j, Expr::Int32)), - ConstantExpr::alloc(value, Expr::Int8))); + ConstantExpr::alloc(j, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } ConstraintManager tmp(bindings); @@ -493,8 +494,6 @@ Solver *klee::createDummySolver() { class STPSolverImpl : public SolverImpl { private: - /// The solver we are part of, for access to public information. - STPSolver *solver; VC vc; STPBuilder *builder; double timeout; @@ -502,7 +501,7 @@ private: SolverRunStatus runStatusCode; public: - STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true); + STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true); ~STPSolverImpl(); char *getConstraintLog(const Query&); @@ -526,9 +525,8 @@ static void stp_error_handler(const char* err_msg) { abort(); } -STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides) - : solver(_solver), - vc(vc_createValidityChecker()), +STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) + : vc(vc_createValidityChecker()), builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0), useForkedSTP(_useForkedSTP), @@ -565,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() { /***/ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides) - : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides)) + : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides)) { } @@ -773,7 +771,6 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, } } } -#include <iostream> bool STPSolverImpl::computeInitialValues(const Query &query, const std::vector<const Array*> |