diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-14 14:54:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-14 21:54:42 +0000 |
commit | 3437ec5c40091503f5c9ba026ce25f813be51d87 (patch) | |
tree | 179ceeceeeb9b3ca8dfe513f5f36f2ac6a2f5add | |
parent | 74c5067d81b8384701cff7f6e7b697d7fe67cf58 (diff) |
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.
-rw-r--r-- | src/main/command_executor.cpp | 11 | ||||
-rwxr-xr-x | 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<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 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], |