diff options
Diffstat (limited to 'test/regress/run_regression.py')
| -rwxr-xr-x | test/regress/run_regression.py | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 759582afc..61b89d9c5 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -161,7 +161,6 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, elif benchmark_ext == '.cvc': pass elif benchmark_ext == '.p': - basic_command_line_args.append('--finite-model-find') status_regex = r'% Status\s*:\s*(Theorem|Unsatisfiable|CounterSatisfiable|Satisfiable)' status_to_output = lambda s: '% SZS status {} for {}'.format(s, benchmark_filename) elif benchmark_ext == '.sy': @@ -214,10 +213,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, if expected_output == '' and expected_error == '': match = None if status_regex: - match = re.search(status_regex, benchmark_content) + match = re.findall(status_regex, benchmark_content) if match: - expected_output = status_to_output(match.group(1)) + expected_output = status_to_output('\n'.join(match)) elif expected_exit_status is None: # If there is no expected output/error and the exit status has not # been set explicitly, the benchmark is invalid. @@ -294,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) |