From c1e7c3a2c53ac80eb07c1359b40151a440b41849 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 15 Mar 2019 13:47:37 +0000 Subject: Placed --rewrite-constraints in the constraint solving category --- lib/Expr/Constraints.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'lib/Expr') 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 - 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 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 src, dst; -- cgit 1.4.1