Add SimplifyExpressions command line option

Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).

1 files changed, 6 insertions, 1 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index abb023eb..fb1a6698 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>
+  SimplifyExpressions("simplify-expressions",
+                     cl::init(true),
+                     cl::desc("Simplify symbolic 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, SimplifyExpressions);
 
   memory = new MemoryManager();
 }