Renamed --use-construct-hash to --use-construct-hash-stp and moved it and use-construct-hash-z3 to the expression building/printing category

2 files changed, 7 insertions, 5 deletions

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 8ec35762..57dea28b 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -44,9 +44,10 @@ using namespace klee;
 
 namespace {
   llvm::cl::opt<bool>
-  UseConstructHash("use-construct-hash", 
-                   llvm::cl::desc("Use hash-consing during STP query construction."),
-                   llvm::cl::init(true));
+  UseConstructHash("use-construct-hash-stp",
+                   llvm::cl::desc("Use hash-consing during STP query construction (default=true)"),
+                   llvm::cl::init(true),
+                   llvm::cl::cat(klee::ExprCat));
 }
 
 ///
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index d03c4c89..06b995ae 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -24,8 +24,9 @@ using namespace klee;
 namespace {
 llvm::cl::opt<bool> UseConstructHashZ3(
     "use-construct-hash-z3",
-    llvm::cl::desc("Use hash-consing during Z3 query construction."),
-    llvm::cl::init(true));
+    llvm::cl::desc("Use hash-consing during Z3 query construction (default=true)"),
+    llvm::cl::init(true),
+    llvm::cl::cat(klee::ExprCat));
 
 // FIXME: This should be std::atomic<bool>. Need C++11 for that.
 bool Z3InterationLogOpen = false;