diff options
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 5efda6b6..74fee290 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -9,6 +9,8 @@ #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" +#include "klee/OptionCategories.h" + #ifdef ENABLE_Z3 #include "Z3Solver.h" #include "Z3Builder.h" @@ -25,19 +27,23 @@ namespace { // the z3 binary to replay all Z3 API calls using its `-log` option. llvm::cl::opt<std::string> Z3LogInteractionFile( "debug-z3-log-api-interaction", llvm::cl::init(""), - llvm::cl::desc("Log API interaction with Z3 to the specified path")); + llvm::cl::desc("Log API interaction with Z3 to the specified path"), + llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt<std::string> Z3QueryDumpFile( "debug-z3-dump-queries", llvm::cl::init(""), - llvm::cl::desc("Dump Z3's representation of the query to the specified path")); + llvm::cl::desc("Dump Z3's representation of the query to the specified path"), + llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt<bool> Z3ValidateModels( "debug-z3-validate-models", llvm::cl::init(false), - llvm::cl::desc("When generating Z3 models validate these against the query")); + llvm::cl::desc("When generating Z3 models validate these against the query"), + llvm::cl::cat(klee::SolvingCat)); llvm::cl::opt<unsigned> Z3VerbosityLevel("debug-z3-verbosity", llvm::cl::init(0), - llvm::cl::desc("Z3 verbosity level (default=0)")); + llvm::cl::desc("Z3 verbosity level (default=0)"), + llvm::cl::cat(klee::SolvingCat)); } #include "llvm/Support/ErrorHandling.h" |