3 files changed, 31 insertions, 26 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 28b786437..ec3e10b5e 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -194,7 +194,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         pExecutor->doCommand(cmd);
       }
       InteractiveShell shell(pExecutor->getSolver(),
-                             pExecutor->getSymbolManager());
+                             pExecutor->getSymbolManager(),
+                             dopts.in(),
+                             dopts.out());
 
       CVC5Message() << Configuration::getPackageName() << " "
                     << Configuration::getVersionString();
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index ea408012a..86f344979 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -85,11 +85,11 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBEDITLINE */
 
-InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
-    : d_solver(solver),
-      d_in(solver->getDriverOptions().in()),
-      d_out(solver->getDriverOptions().out()),
-      d_quit(false)
+InteractiveShell::InteractiveShell(api::Solver* solver,
+                                   SymbolManager* sm,
+                                   std::istream& in,
+                                   std::ostream& out)
+    : d_solver(solver), d_in(in), d_out(out), d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, true);
   /* Create parser with bogus input. */
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index bf05a1ec7..6029d6b0e 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -35,6 +35,29 @@ class SymbolManager;
 
 class InteractiveShell
 {
+ public:
+  InteractiveShell(api::Solver* solver,
+                   SymbolManager* sm,
+                   std::istream& in,
+                   std::ostream& out);
+
+  /**
+   * Close out the interactive session.
+   */
+  ~InteractiveShell();
+
+  /**
+   * Read a command from the interactive shell. This will read as
+   * many lines as necessary to parse a well-formed command.
+   */
+  Command* readCommand();
+
+  /**
+   * Return the internal parser being used.
+   */
+  parser::Parser* getParser() { return d_parser; }
+
+ private:
   api::Solver* d_solver;
   std::istream& d_in;
   std::ostream& d_out;
@@ -46,26 +69,6 @@ class InteractiveShell
 
   static const std::string INPUT_FILENAME;
   static const unsigned s_historyLimit = 500;
-
-public:
- InteractiveShell(api::Solver* solver, SymbolManager* sm);
-
- /**
-  * Close out the interactive session.
-  */
- ~InteractiveShell();
-
- /**
-  * Read a command from the interactive shell. This will read as
-  * many lines as necessary to parse a well-formed command.
-  */
- Command* readCommand();
-
- /**
-  * Return the internal parser being used.
-  */
- parser::Parser* getParser() { return d_parser; }
-
 };/* class InteractiveShell */
 
 }  // namespace cvc5