diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-14 14:17:06 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-14 14:17:06 -0700 |
commit | 86460c41713243e0018e3038bcba5d053156b8b6 (patch) | |
tree | 483a41801908d440c5991c1aae69c30af70127b3 /test/regress | |
parent | bfe17bb07882e869c58a7b6961970d7198d0e98d (diff) |
fix
Diffstat (limited to 'test/regress')
-rwxr-xr-x | test/regress/run_regression.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 34b9c7fdb..c3e21e6ec 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -141,7 +141,7 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary, exit_status = None if dump: dump_args = [ - '--parse-only', '--output-lang=smt2' + '--parse-only', '-o', 'raw-benchmark', '--output-lang=smt2' ] dump_output, _, _ = run_process( bin_args + command_line + dump_args + [benchmark_filename], |