1 files changed, 10 insertions, 6 deletions
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 417cfa94d..af6960ff7 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -27,6 +27,7 @@
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/parser_builder.h"
+#include "parser/symbol_manager.h"
 #include "smt/command.h"
 
 using namespace CVC4;
@@ -42,7 +43,9 @@ class InteractiveShellBlack : public CxxTest::TestSuite
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
+    d_symman.reset(nullptr);
     d_solver.reset(new api::Solver(&d_options));
+    d_symman.reset(new parser::SymbolManager(d_solver.get()));
   }
 
   void tearDown() override
@@ -53,18 +56,18 @@ class InteractiveShellBlack : public CxxTest::TestSuite
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
     /* readCommand may return a sequence, so we can't say for sure
        whether it will return 1 or 2... */
@@ -72,7 +75,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite
   }
 
   void testDefUse2() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -82,20 +85,21 @@ class InteractiveShellBlack : public CxxTest::TestSuite
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }
 
  private:
   std::unique_ptr<api::Solver> d_solver;
+  std::unique_ptr<parser::SymbolManager> d_symman;
   Options d_options;
   stringstream* d_sin;
   stringstream* d_sout;