Pass symbol manager to commands (#5410)

[cvc5.git] / src / main / command_executor.cpp

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a56210fb1d08a8414527af38abeec2628e6b6a52..7b20f3a1aec85eb9830828143b4eac3503dc2f57 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -119,9 +119,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options.getVerbosity() >= -1) {
-    status = solverInvoke(d_solver.get(), cmd, d_options.getOut());
+    status =
+        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
   } else {
-    status = solverInvoke(d_solver.get(), cmd, nullptr);
+    status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
   }
 
   api::Result res;
@@ -198,15 +199,18 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   return status;
 }
 
-bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out)
+bool solverInvoke(api::Solver* solver,
+                  parser::SymbolManager* sm,
+                  Command* cmd,
+                  std::ostream* out)
 {
   if (out == NULL)
   {
-    cmd->invoke(solver);
+    cmd->invoke(solver, sm);
   }
   else
   {
-    cmd->invoke(solver, *out);
+    cmd->invoke(solver, sm, *out);
   }
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =