Make `-o raw-benchmark` work with `--parse-only` (#7195)

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.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index ad0d24143293c779623b63b6b25185e1b1368aff..6b03f82e303881b271f185de0bb57ca2bcc40c3c 100644 (file)
--- 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 =

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 4c9ea3fcb733897b7cd447ca0b4adf260d608c93..c3e21e6ec56ee184d7048c89c4126bb83e959daa 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -141,8 +141,7 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary,
     exit_status = None
     if dump:
         dump_args = [
-            '--preprocess-only', '-o', 'raw-benchmark',
-            '--output-lang=smt2', '-qq'
+            '--parse-only', '-o', 'raw-benchmark', '--output-lang=smt2'
         ]
         dump_output, _, _ = run_process(
             bin_args + command_line + dump_args + [benchmark_filename],