From 4046c8e7cbd5b9db8562344c21c15c3db6248e7d Mon Sep 17 00:00:00 2001
From: ahorn <alex.horn@cs.ox.ac.uk>
Date: Mon, 12 May 2014 15:13:56 +0100
Subject: Add SimplifyExpressions command line option

Allow users to bypass ConstraintManager::simplifyExpr(ref<Expr>).
---
 lib/Core/Executor.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'lib/Core')

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();
 }
-- 
cgit 1.4.1