aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp7
1 files changed, 6 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 3a07138d..fcdf8a6d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -164,6 +164,11 @@ namespace {
SimplifySymIndices("simplify-sym-indices",
cl::init(false));
+ cl::opt<bool>
+ EqualitySubstitution("equality-substitution",
+ cl::init(true),
+ cl::desc("Simplify equality expressions before querying the solver (default=on)."));
+
cl::opt<unsigned>
MaxSymArraySize("max-sym-array-size",
cl::init(0));
@@ -333,7 +338,7 @@ Executor::Executor(const InterpreterOptions &opts,
interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME),
interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME));
- this->solver = new TimingSolver(solver);
+ this->solver = new TimingSolver(solver, EqualitySubstitution);
memory = new MemoryManager();
}