summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-09-14 14:17:06 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2021-09-14 14:17:06 -0700
commit86460c41713243e0018e3038bcba5d053156b8b6 (patch)
tree483a41801908d440c5991c1aae69c30af70127b3 /test/regress
parentbfe17bb07882e869c58a7b6961970d7198d0e98d (diff)
fix
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