3 files changed, 44 insertions, 34 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5dbc50592..9db704621 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,7 +24,6 @@
 #include <string>
 #include <vector>
 
-#include "api/cvc4cpp.h"
 #include "main/main.h"
 #include "smt/command.h"
 
@@ -49,14 +48,15 @@ void setNoLimitCPU() {
 
 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
 
-CommandExecutor::CommandExecutor(api::Solver* solver, Options& options)
-    : d_solver(solver),
+CommandExecutor::CommandExecutor(Options& options)
+    : d_solver(new api::Solver(&options)),
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
       d_result(),
-      d_replayStream(NULL)
-{}
+      d_replayStream(nullptr)
+{
+}
 
 void CommandExecutor::flushStatistics(std::ostream& out) const
 {
@@ -112,7 +112,13 @@ void CommandExecutor::reset()
   {
     flushStatistics(*d_options.getErr());
   }
-  d_solver->reset();
+  /* We have to keep options passed via CL on reset. These options are stored
+   * in CommandExecutor::d_options (populated and created in the driver), and
+   * CommandExecutor::d_options only contains *these* options since the
+   * NodeManager copies the options into a new options object before SmtEngine
+   * configures additional options based on the given CL options.
+   * We can thus safely reuse CommandExecutor::d_options here. */
+  d_solver.reset(new api::Solver(&d_options));
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 3688f592f..3fc971f5b 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -18,6 +18,7 @@
 #include <iosfwd>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
 #include "smt/command.h"
@@ -32,27 +33,28 @@ class Solver;
 
 namespace main {
 
-class CommandExecutor {
-private:
+class CommandExecutor
+{
+ private:
   std::string d_lastStatistics;
 
-protected:
- api::Solver* d_solver;
- SmtEngine* d_smtEngine;
- Options& d_options;
- StatisticsRegistry d_stats;
- Result d_result;
- ExprStream* d_replayStream;
-
-public:
- CommandExecutor(api::Solver* solver, Options& options);
-
- virtual ~CommandExecutor()
- {
-   if (d_replayStream != NULL)
-   {
-     delete d_replayStream;
-   }
+ protected:
+  std::unique_ptr<api::Solver> d_solver;
+  SmtEngine* d_smtEngine;
+  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;
+    }
   }
 
   /**
@@ -62,6 +64,9 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
+  /** Get a pointer to the solver object owned by this CommandExecutor. */
+  api::Solver* getSolver() { return d_solver.get(); }
+
   Result getResult() const { return d_result; }
   void reset();
 
@@ -96,7 +101,7 @@ protected:
 private:
   CommandExecutor();
 
-};/* class CommandExecutor */
+}; /* class CommandExecutor */
 
 bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index b999fe4b0..be2d0a0f8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -181,16 +181,15 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // important even for muzzled builds (to get result output right)
   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 
-  // Create the expression manager using appropriate options
-  std::unique_ptr<api::Solver> solver;
-  solver.reset(new api::Solver(&opts));
-  pExecutor = new CommandExecutor(solver.get(), 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(solver.get(), replayFilename, opts);
+    ParserBuilder replayParserBuilder(
+        pExecutor->getSolver(), replayFilename, opts);
 
     if( replayFilename == "-") {
       if( inputFromStdin ) {
@@ -229,7 +228,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         pExecutor->doCommand(cmd);
         delete cmd;
       }
-      InteractiveShell shell(solver.get());
+      InteractiveShell shell(pExecutor->getSolver());
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
@@ -282,7 +281,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // delete cmd;
       }
 
-      ParserBuilder parserBuilder(solver.get(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -443,7 +442,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 
-      ParserBuilder parserBuilder(solver.get(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)