3 files changed, 1 insertions, 44 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 9db704621..323f24492 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -53,8 +53,7 @@ CommandExecutor::CommandExecutor(Options& options)
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
-      d_result(),
-      d_replayStream(nullptr)
+      d_result()
 {
 }
 
@@ -72,12 +71,6 @@ void CommandExecutor::safeFlushStatistics(int fd) const
   d_stats.safeFlushInformation(fd);
 }
 
-void CommandExecutor::setReplayStream(ExprStream* replayStream) {
-  assert(d_replayStream == NULL);
-  d_replayStream = replayStream;
-  d_smtEngine->setReplayStream(d_replayStream);
-}
-
 bool CommandExecutor::doCommand(Command* cmd)
 {
   if( d_options.getParseOnly() ) {
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);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index be2d0a0f8..92368148b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -184,23 +184,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // Create the command executor to execute the parsed commands
   pExecutor = new CommandExecutor(opts);
 
-  std::unique_ptr<Parser> replayParser;
-  if (opts.getReplayInputFilename() != "")
-  {
-    std::string replayFilename = opts.getReplayInputFilename();
-    ParserBuilder replayParserBuilder(
-        pExecutor->getSolver(), replayFilename, opts);
-
-    if( replayFilename == "-") {
-      if( inputFromStdin ) {
-        throw OptionException("Replay file and input file can't both be stdin.");
-      }
-      replayParserBuilder.withStreamInput(cin);
-    }
-    replayParser.reset(replayParserBuilder.build());
-    pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get()));
-  }
-
   int returnValue = 0;
   {
     // Timer statistic
@@ -241,10 +224,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                   << endl << endl;
         Message() << Configuration::copyright() << endl;
       }
-      if(replayParser) {
-        // have the replay parser use the declarations input interactively
-        replayParser->useDeclarationsFrom(shell.getParser());
-      }
 
       while(true) {
         try {
@@ -294,10 +273,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       vector< vector<Command*> > allCommands;
       allCommands.push_back(vector<Command*>());
       std::unique_ptr<Parser> parser(parserBuilder.build());
-      if(replayParser) {
-        // have the replay parser use the file's declarations
-        replayParser->useDeclarationsFrom(parser.get());
-      }
       int needReset = 0;
       // true if one of the commands was interrupted
       bool interrupted = false;
@@ -453,10 +428,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
 
       std::unique_ptr<Parser> parser(parserBuilder.build());
-      if(replayParser) {
-        // have the replay parser use the file's declarations
-        replayParser->useDeclarationsFrom(parser.get());
-      }
       bool interrupted = false;
       while (status)
       {