diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2019-03-15 13:47:37 +0000 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2019-03-15 22:53:39 +0000 |
commit | c1e7c3a2c53ac80eb07c1359b40151a440b41849 (patch) | |
tree | 013f45626699cb42fbc3f2395d8c0af54d971e9f | |
parent | 43088bcc6323c3a3ef394ac909ed3cc0a909d249 (diff) | |
download | klee-c1e7c3a2c53ac80eb07c1359b40151a440b41849.tar.gz |
Placed --rewrite-constraints in the constraint solving category
-rw-r--r-- | lib/Expr/Constraints.cpp | 14 |
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; |