aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Z3Solver.cpp14
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"