diff options
| -rw-r--r-- | include/klee/Solver.h | 2 | ||||
| -rw-r--r-- | include/klee/SolverCmdLine.h | 12 |
2 files changed, 6 insertions, 8 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 2b80e9ec..c2a8ef1e 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -11,7 +11,7 @@ #define KLEE_SOLVER_H #include "klee/Expr.h" -#include "klee/SolverCmdLine.h" // FIXME: This is just for CoreSolverType +#include "klee/SolverCmdLine.h" #include <vector> diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h index 7a122e72..19e5fae6 100644 --- a/include/klee/SolverCmdLine.h +++ b/include/klee/SolverCmdLine.h @@ -42,14 +42,12 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; extern llvm::cl::opt<bool> UseAssignmentValidatingSolver; -/// The different query logging solvers that can switched on/off +/// The different query logging solvers that can be switched on/off enum QueryLoggingSolverType { - ALL_KQUERY, ///< Log all queries (un-optimised) in .kquery (KQuery) format - ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format - SOLVER_KQUERY, ///< Log queries passed to solver (optimised) in .kquery - ///< (KQuery) format - SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 - ///< (SMT-LIBv2) format + ALL_KQUERY, ///< Log all queries in .kquery (KQuery) format + ALL_SMTLIB, ///< Log all queries .smt2 (SMT-LIBv2) format + SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format + SOLVER_SMTLIB ///< Log queries passed to solver in .smt2 (SMT-LIBv2) format }; extern llvm::cl::bits<QueryLoggingSolverType> queryLoggingOptions; |