summaryrefslogtreecommitdiff
path: root/test/regress/run_regression.py
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-08-13 10:39:45 -0500
committerGitHub <noreply@github.com>2019-08-13 10:39:45 -0500
commit47b910a85de71b6617e4d1d210dcb57de597961b (patch)
tree2319441716ca0c10042e011579c67814334fd5b3 /test/regress/run_regression.py
parent2267c5050fafde26b34dc1e84de015617efa7cc7 (diff)
Implement check abduct feature (#3152)
Diffstat (limited to 'test/regress/run_regression.py')
-rwxr-xr-xtest/regress/run_regression.py4
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 8918c75c1..61b89d9c5 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -293,6 +293,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
'--unconstrained-simp' not in all_args and \
not cvc4_binary.endswith('pcvc4'):
extra_command_line_args += ['--check-unsat-cores']
+ if '--no-check-abducts' not in all_args and \
+ '--check-abducts' not in all_args and \
+ not cvc4_binary.endswith('pcvc4'):
+ extra_command_line_args += ['--check-abducts']
if extra_command_line_args:
command_line_args_configs.append(all_args +
extra_command_line_args)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback