about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/CommandLine.h6
-rw-r--r--include/klee/Common.h2
-rw-r--r--include/klee/IncompleteSolver.h2
-rw-r--r--include/klee/Solver.h13
-rw-r--r--include/klee/SolverImpl.h9
-rw-r--r--lib/Basic/CmdLineOptions.cpp17
-rw-r--r--lib/Basic/ConstructSolverChain.cpp14
-rw-r--r--lib/Core/Executor.cpp43
-rw-r--r--lib/Core/Executor.h5
-rw-r--r--lib/Core/Memory.cpp2
-rw-r--r--lib/Core/TimingSolver.h15
-rw-r--r--lib/Solver/CachingSolver.cpp10
-rw-r--r--lib/Solver/CexCachingSolver.cpp12
-rw-r--r--lib/Solver/IncompleteSolver.cpp9
-rw-r--r--lib/Solver/IndependentSolver.cpp10
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp7
-rw-r--r--lib/Solver/QueryLoggingSolver.h3
-rw-r--r--lib/Solver/Solver.cpp28
-rw-r--r--test/Feature/SolverTimeout.c2
-rw-r--r--tools/kleaver/main.cpp24
20 files changed, 156 insertions, 77 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index f303ae6c..38b22c6f 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -22,7 +22,11 @@ extern llvm::cl::opt<bool> DebugValidateSolver;
   
 extern llvm::cl::opt<int> MinQueryTimeToLog;
 
-extern llvm::cl::opt<double> MaxSTPTime;
+extern llvm::cl::opt<double> MaxCoreSolverTime;
+
+extern llvm::cl::opt<bool> UseForkedCoreSolver;
+
+extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 1418f1b6..7149708a 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -22,7 +22,7 @@ namespace klee {
     const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
     const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
 
-    Solver *constructSolverChain(STPSolver *stpSolver,
+    Solver *constructSolverChain(Solver *coreSolver,
                                  std::string querySMT2LogPath,
                                  std::string baseSolverQuerySMT2LogPath,
                                  std::string queryPCLogPath,
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index 9a122c74..f589e3b3 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -102,6 +102,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 }
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 1af30870..8fe33c7c 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -194,6 +194,9 @@ namespace klee {
     //
     // FIXME: This should go into a helper class, and should handle failure.
     virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
+    
+    virtual char *getConstraintLog(const Query& query);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /// STPSolver - A complete solver based on STP.
@@ -207,15 +210,13 @@ namespace klee {
     /// be optimized into add/shift/multiply operations.
     STPSolver(bool useForkedSTP, bool optimizeDivides = true);
 
-    
-    
     /// getConstraintLog - Return the constraint log for the given state in CVC
     /// format.
-    char *getConstraintLog(const Query&);
-    
-    /// setTimeout - Set constraint solver timeout delay to the given value; 0
+    virtual char *getConstraintLog(const Query&);
+
+    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0
     /// is off.
-    void setTimeout(double timeout);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /* *** */
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index e200205b..c17082a8 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -93,10 +93,17 @@ namespace klee {
     
     /// getOperationStatusCode - get the status of the last solver operation
     virtual SolverRunStatus getOperationStatusCode() = 0;
-    
+
     /// getOperationStatusString - get string representation of the operation
     /// status code
     static const char* getOperationStatusString(SolverRunStatus statusCode);
+
+    virtual char *getConstraintLog(const Query& query)  {
+        // dummy
+        return(NULL);
+    }
+
+    virtual void setCoreSolverTimeout(double timeout) {};
 };
 
 }
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 6fe20b7e..ac0474fb 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -40,9 +40,20 @@ MinQueryTimeToLog("min-query-time-to-log",
                                  "Set this param to a negative value to log timeouts only."));
 
 llvm::cl::opt<double>
-MaxSTPTime("max-stp-time",
-           llvm::cl::desc("Maximum amount of time for a single query (default=0s (off)). Enables --use-forked-stp"),
-           llvm::cl::init(0.0));
+MaxCoreSolverTime("max-solver-time",
+           llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"),
+           llvm::cl::init(0.0),
+           llvm::cl::value_desc("seconds"));
+
+llvm::cl::opt<bool>
+UseForkedCoreSolver("use-forked-solver",
+             llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"),
+             llvm::cl::init(true));
+
+llvm::cl::opt<bool>
+CoreSolverOptimizeDivides("solver-optimize-divides", 
+                 llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"),
+                 llvm::cl::init(true));
 
 
 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 70c728df..c0d0ef61 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -16,13 +16,13 @@
 
 namespace klee
 {
-	Solver *constructSolverChain(STPSolver *stpSolver,
-								 std::string querySMT2LogPath,
-								 std::string baseSolverQuerySMT2LogPath,
-								 std::string queryPCLogPath,
-								 std::string baseSolverQueryPCLogPath)
+        Solver *constructSolverChain(Solver *coreSolver,
+                                     std::string querySMT2LogPath,
+                                     std::string baseSolverQuerySMT2LogPath,
+                                     std::string queryPCLogPath,
+                                     std::string baseSolverQueryPCLogPath)
 	{
-	  Solver *solver = stpSolver;
+	  Solver *solver = coreSolver;
 
 	  if (optionIsSet(queryLoggingOptions, SOLVER_PC))
 	  {
@@ -55,7 +55,7 @@ namespace klee
 		solver = createIndependentSolver(solver);
 
 	  if (DebugValidateSolver)
-		solver = createValidatingSolver(solver, stpSolver);
+		solver = createValidatingSolver(solver, coreSolver);
 
 	  if (optionIsSet(queryLoggingOptions, ALL_PC))
 	  {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d0ad811d..b57b1956 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -189,7 +189,7 @@ namespace {
 
   cl::opt<double>
   MaxInstructionTime("max-instruction-time",
-                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-stp"),
+                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"),
                      cl::init(0));
   
   cl::opt<double>
@@ -221,16 +221,6 @@ namespace {
   MaxMemoryInhibit("max-memory-inhibit",
             cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"),
             cl::init(true));
-
-  cl::opt<bool>
-  UseForkedSTP("use-forked-stp",
-	       cl::desc("Run STP in a forked process (default=off)"));
-
-  cl::opt<bool>
-  STPOptimizeDivides("stp-optimize-divides", 
-                 cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"),
-                 cl::init(true));
-
 }
 
 
@@ -258,19 +248,20 @@ Executor::Executor(const InterpreterOptions &opts,
     inhibitForking(false),
     haltExecution(false),
     ivcEnabled(false),
-    stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0
-      ? std::min(MaxSTPTime,MaxInstructionTime)
-      : std::max(MaxSTPTime,MaxInstructionTime)) {
-  if (stpTimeout) UseForkedSTP = true;
-  STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
+    coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
+      ? std::min(MaxCoreSolverTime,MaxInstructionTime)
+      : std::max(MaxCoreSolverTime,MaxInstructionTime)) {
+      
+  if (coreSolverTimeout) UseForkedCoreSolver = true;
+  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();
 }
@@ -666,7 +657,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     }
   }
 
-  double timeout = stpTimeout;
+  double timeout = coreSolverTimeout;
   if (isSeeding)
     timeout *= it->second.size();
   solver->setTimeout(timeout);
@@ -982,7 +973,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
     ref<ConstantExpr> value;
     bool isTrue = false;
 
-    solver->setTimeout(stpTimeout);      
+    solver->setTimeout(coreSolverTimeout);      
     if (solver->getValue(state, e, value) &&
         solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) &&
         isTrue)
@@ -2979,7 +2970,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // fast path: single in-bounds resolution
   ObjectPair op;
   bool success;
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
   if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
     address = toConstant(state, address, "resolveOne failure");
     success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
@@ -2996,7 +2987,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     ref<Expr> offset = mo->getOffsetExpr(address);
 
     bool inBounds;
-    solver->setTimeout(stpTimeout);
+    solver->setTimeout(coreSolverTimeout);
     bool success = solver->mustBeTrue(state, 
                                       mo->getBoundsCheckOffset(offset, bytes),
                                       inBounds);
@@ -3035,9 +3026,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   // resolution with out of bounds)
   
   ResolutionList rl;  
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
   bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
-                                               0, stpTimeout);
+                                               0, coreSolverTimeout);
   solver->setTimeout(0);
   
   // XXX there is some query wasteage here. who cares?
@@ -3290,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);
   }
@@ -3328,7 +3319,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
                                    std::pair<std::string,
                                    std::vector<unsigned char> > >
                                    &res) {
-  solver->setTimeout(stpTimeout);
+  solver->setTimeout(coreSolverTimeout);
 
   ExecutionState tmp(state);
   if (!NoPreferCex) {
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index c434c34c..a9d6b791 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -173,8 +173,9 @@ private:
   /// false, it is buggy (it needs to validate its writes).
   bool ivcEnabled;
 
-  /// The maximum time to allow for a single stp query.
-  double stpTimeout;  
+  /// The maximum time to allow for a single core solver query.
+  /// (e.g. for a single STP query)
+  double coreSolverTimeout; 
 
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 7b3655f8..08c95d48 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -110,6 +110,7 @@ ObjectState::ObjectState(const MemoryObject *mo)
     const Array *array = new Array("tmp_arr" + llvm::utostr(++id), size);
     updates = UpdateList(array, 0);
   }
+  memset(concreteStore, 0, size);
 }
 
 
@@ -126,6 +127,7 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
     readOnly(false) {
   mo->refCount++;
   makeSymbolic();
+  memset(concreteStore, 0, size);
 }
 
 ObjectState::ObjectState(const ObjectState &os) 
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b13879df..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,18 @@ 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->setTimeout(t);
+      solver->setCoreSolverTimeout(t);
+    }
+    
+    char *getConstraintLog(const Query& query) {
+      return solver->getConstraintLog(query);
     }
 
     bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5911bbf3..674d4627 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -85,6 +85,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -244,6 +246,14 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 497ccb4a..df7fffc5 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -31,7 +31,7 @@ namespace {
 
   cl::opt<bool>
   CexCacheTryAll("cex-cache-try-all",
-                 cl::desc("try substituting all counterexamples before asking STP"),
+                 cl::desc("try substituting all counterexamples before asking the SMT solver"),
                  cl::init(false));
 
   cl::opt<bool>
@@ -83,6 +83,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query& query);
+  void setCoreSolverTimeout(double timeout);
 };
 
 ///
@@ -350,6 +352,14 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CexCachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CexCachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 7bc8058d..dc2c9fd4 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -138,3 +138,12 @@ StagedSolverImpl::computeInitialValues(const Query& query,
 SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() {
   return secondary->impl->getOperationStatusCode();
 }
+
+char *StagedSolverImpl::getConstraintLog(const Query& query) {
+  return secondary->impl->getConstraintLog(query);
+}
+
+void StagedSolverImpl::setCoreSolverTimeout(double timeout) {
+  secondary->impl->setCoreSolverTimeout(timeout);
+}
+
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index b3ef1e57..d9fc77dc 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -285,6 +285,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -318,6 +320,14 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();      
 }
 
+char *IndependentSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void IndependentSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createIndependentSolver(Solver *s) {
   return new Solver(new IndependentSolver(s));
 }
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 245ad3bf..e7187fc3 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -183,4 +183,11 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *QueryLoggingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
 
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 527d075b..2c7d80e8 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -70,7 +70,8 @@ public:
                               std::vector< std::vector<unsigned char> > &values,
                               bool &hasSolution);
     SolverRunStatus getOperationStatusCode();
-
+    char *getConstraintLog(const Query&);
+    void setCoreSolverTimeout(double timeout);
 };
 
 #endif	/* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index b3d1613d..3414cda2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -101,6 +101,14 @@ Solver::~Solver() {
   delete impl; 
 }
 
+char *Solver::getConstraintLog(const Query& query) {
+    return impl->getConstraintLog(query);
+}
+
+void Solver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
+}
+
 bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
@@ -307,6 +315,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 bool ValidatingSolver::computeTruth(const Query& query,
@@ -408,6 +418,14 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *ValidatingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
   return new Solver(new ValidatingSolver(s, oracle));
 }
@@ -466,9 +484,9 @@ private:
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
-
+  
   char *getConstraintLog(const Query&);
-  void setTimeout(double _timeout) { timeout = _timeout; }
+  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
 
   bool computeTruth(const Query&, bool &isValid);
   bool computeValue(const Query&, ref<Expr> &result);
@@ -532,11 +550,11 @@ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
 }
 
 char *STPSolver::getConstraintLog(const Query &query) {
-  return static_cast<STPSolverImpl*>(impl)->getConstraintLog(query);  
+  return impl->getConstraintLog(query);  
 }
 
-void STPSolver::setTimeout(double timeout) {
-  static_cast<STPSolverImpl*>(impl)->setTimeout(timeout);
+void STPSolver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
 }
 
 /***/
diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c
index 96f75cd7..34405c1f 100644
--- a/test/Feature/SolverTimeout.c
+++ b/test/Feature/SolverTimeout.c
@@ -1,5 +1,5 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
-// RUN: %klee --max-stp-time=1 %t1.bc
+// RUN: %klee --max-solver-time=1 %t1.bc
 #include <stdio.h>
 
 int main() {
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 5b9e43a6..accc48e4 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -211,25 +211,19 @@ static bool EvaluateInputAST(const char *Filename,
     return false;
 
   // FIXME: Support choice of solver.
-  Solver *S   = 0;
-  Solver *STP = 0;
+  Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
+  
   if (!UseDummySolver) {
-    STPSolver* stpSolver = new STPSolver(true);
-    if (0 != MaxSTPTime) {
-      stpSolver->setTimeout(MaxSTPTime);    
+    if (0 != MaxCoreSolverTime) {
+      coreSolver->setCoreSolverTimeout(MaxCoreSolverTime);
     }
-    STP = S = stpSolver;
-  }
-  else {
-    STP = S = createDummySolver(); 
   }
 
-  S= constructSolverChain((STPSolver*) STP,
-		  	  	  	      getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
-		  	  	  	      getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
-		  	  	  	      getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
-		  	  	  	      getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
-
+  Solver *S = constructSolverChain(coreSolver,
+                                   getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
+                                   getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
+                                   getQueryLogPath(ALL_QUERIES_PC_FILE_NAME),
+                                   getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME));
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 06:57:26 +0000