summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress')
-rwxr-xr-xtest/regress/run_regression.py2
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],
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback