1 files changed, 0 insertions, 29 deletions
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)
       {