diff options
Diffstat (limited to 'lib/Core')
| -rw-r--r-- | lib/Core/Executor.cpp | 9 | ||||
| -rw-r--r-- | lib/Core/TimingSolver.h | 11 |
2 files changed, 9 insertions, 11 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 309c5fd5..b57b1956 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -251,16 +251,17 @@ Executor::Executor(const InterpreterOptions &opts, coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 ? std::min(MaxCoreSolverTime,MaxInstructionTime) : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; - STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = - constructSolverChain(stpSolver, + constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver, stpSolver); + this->solver = new TimingSolver(solver); memory = new MemoryManager(); } @@ -3280,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state, case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); + char *log = solver->getConstraintLog(query); res = std::string(log); free(log); } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 2684e071..c98dd881 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -17,15 +17,13 @@ namespace klee { class ExecutionState; - class Solver; - class STPSolver; + class Solver; /// TimingSolver - A simple class which wraps a solver and handles /// tracking the statistics that we care about. class TimingSolver { public: Solver *solver; - STPSolver *stpSolver; bool simplifyExprs; public: @@ -34,15 +32,14 @@ namespace klee { /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, STPSolver *_stpSolver, - bool _simplifyExprs = true) - : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {} + TimingSolver(Solver *_solver, bool _simplifyExprs = true) + : solver(_solver), simplifyExprs(_simplifyExprs) {} ~TimingSolver() { delete solver; } void setTimeout(double t) { - stpSolver->setCoreSolverTimeout(t); + solver->setCoreSolverTimeout(t); } char *getConstraintLog(const Query& query) { |