diff options
Diffstat (limited to 'lib/Basic/ConstructSolverChain.cpp')
-rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 5880ad59..8341f62d 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -13,8 +13,10 @@ #include "klee/Common.h" #include "klee/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Internal/System/Time.h" #include "llvm/Support/raw_ostream.h" + namespace klee { Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, @@ -22,17 +24,16 @@ Solver *constructSolverChain(Solver *coreSolver, std::string queryKQueryLogPath, std::string baseSolverQueryKQueryLogPath) { Solver *solver = coreSolver; + const time::Span minQueryTimeToLog(MinQueryTimeToLog); if (queryLoggingOptions.isSet(SOLVER_KQUERY)) { - solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, - MinQueryTimeToLog); + solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging queries that reach solver in .kquery format to %s\n", baseSolverQueryKQueryLogPath.c_str()); } if (queryLoggingOptions.isSet(SOLVER_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, - MinQueryTimeToLog); + solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging queries that reach solver in .smt2 format to %s\n", baseSolverQuerySMT2LogPath.c_str()); } @@ -56,15 +57,13 @@ Solver *constructSolverChain(Solver *coreSolver, solver = createValidatingSolver(solver, coreSolver); if (queryLoggingOptions.isSet(ALL_KQUERY)) { - solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, - MinQueryTimeToLog); + solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging all queries in .kquery format to %s\n", queryKQueryLogPath.c_str()); } if (queryLoggingOptions.isSet(ALL_SMTLIB)) { - solver = - createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog); + solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries); klee_message("Logging all queries in .smt2 format to %s\n", querySMT2LogPath.c_str()); } |