about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2019-03-15 13:47:37 +0000
committerMartinNowack <martin.nowack@gmail.com>2019-03-15 22:53:39 +0000
commitc1e7c3a2c53ac80eb07c1359b40151a440b41849 (patch)
tree013f45626699cb42fbc3f2395d8c0af54d971e9f
parent43088bcc6323c3a3ef394ac909ed3cc0a909d249 (diff)
downloadklee-c1e7c3a2c53ac80eb07c1359b40151a440b41849.tar.gz
Placed --rewrite-constraints in the constraint solving category
-rw-r--r--lib/Expr/Constraints.cpp14
1 files changed, 8 insertions, 6 deletions
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 8bf6bc58..e033333b 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -9,9 +9,10 @@
 
 #include "klee/Constraints.h"
 
+#include "klee/Internal/Module/KModule.h"
+#include "klee/OptionCategories.h"
 #include "klee/util/ExprPPrinter.h"
 #include "klee/util/ExprVisitor.h"
-#include "klee/Internal/Module/KModule.h"
 
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
@@ -21,13 +22,14 @@
 using namespace klee;
 
 namespace {
-  llvm::cl::opt<bool>
-  RewriteEqualities("rewrite-equalities",
-		    llvm::cl::init(true),
-		    llvm::cl::desc("Rewrite existing constraints when an equality with a constant is added (default=true)"));
+llvm::cl::opt<bool> RewriteEqualities(
+    "rewrite-equalities",
+    llvm::cl::desc("Rewrite existing constraints when an equality with a "
+                   "constant is added (default=true)"),
+    llvm::cl::init(true),
+    llvm::cl::cat(SolvingCat));
 }
 
-
 class ExprReplaceVisitor : public ExprVisitor {
 private:
   ref<Expr> src, dst;