Make `-o raw-benchmark` work with `--parse-only`

Before, cvc5 was returning with `--parse-only` before the code could
reach the code responsible for dumping the raw benchmark. This moves the
check for `--parse-only` to the appropriate place and updates the
`run_regression.py` script to use `--parse-only`.

1 files changed, 6 insertions, 5 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index ad0d24143..6b03f82e3 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -87,11 +87,6 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if (d_solver->getOptionInfo("parse-only").boolValue())
-  {
-    return true;
-  }
-
   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
   if(seq != nullptr) {
     // assume no error
@@ -203,6 +198,12 @@ bool solverInvoke(api::Solver* solver,
     std::ostream& ss = solver->getOutput("raw-benchmark");
     cmd->toStream(ss);
   }
+
+  if (solver->getOptionInfo("parse-only").boolValue())
+  {
+    return true;
+  }
+
   cmd->invoke(solver, sm, out);
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =