Renamed --use-construct-hash to --use-construct-hash-stp and moved it…

… and use-construct-hash-z3 to the expression building/printing category
chao-peng · Mar 13, 2019 · 6da5297 · 6da5297
1 parent adead52
commit 6da5297
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git 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
@@ -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;