diff options
Diffstat (limited to 'src/main/command_executor.h')
-rw-r--r-- | src/main/command_executor.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 3fc971f5b..a9b6d9077 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -44,17 +44,12 @@ class CommandExecutor Options& d_options; StatisticsRegistry d_stats; Result d_result; - ExprStream* d_replayStream; public: CommandExecutor(Options& options); virtual ~CommandExecutor() { - if (d_replayStream != NULL) - { - delete d_replayStream; - } } /** @@ -92,8 +87,6 @@ class CommandExecutor void flushOutputStreams(); - void setReplayStream(ExprStream* replayStream); - protected: /** Executes treating cmd as a singleton */ virtual bool doCommandSingleton(CVC4::Command* cmd); |