Added Z3 options to the constraint solving category

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"