about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core/Executor.h')
-rw-r--r--lib/Core/Executor.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index ec2d49c0..6a640905 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -16,6 +16,7 @@
 #define KLEE_EXECUTOR_H
 
 #include "klee/ExecutionState.h"
+#include "klee/ArrayExprOptimizer.h"
 #include "klee/Interpreter.h"
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
@@ -228,6 +229,9 @@ private:
   // @brief buffer to store logs before flushing to file
   llvm::raw_string_ostream debugLogBuffer;
 
+  /// Optimizes expressions
+  ExprOptimizer optimizer;
+
   llvm::Function* getTargetFunction(llvm::Value *calledVal,
                                     ExecutionState &state);