From 3437ec5c40091503f5c9ba026ce25f813be51d87 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 14 Sep 2021 14:54:42 -0700 Subject: [PATCH] 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. --- src/main/command_executor.cpp | 11 ++++++----- test/regress/run_regression.py | 3 +-- 2 files changed, 7 insertions(+), 7 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(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 4c9ea3fcb..c3e21e6ec 100755 --- 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], -- 2.30.2