diff options
| -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..34b9c7fdb 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', '--output-lang=smt2' ] dump_output, _, _ = run_process( bin_args + command_line + dump_args + [benchmark_filename], |