diff options
Diffstat (limited to 'test/regress/run_regression.py')
| -rwxr-xr-x | test/regress/run_regression.py | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index c3e21e6ec..32ba6f6c2 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -203,8 +203,6 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, elif benchmark_ext == '.smt2': status_regex = r'set-info\s*:status\s*(sat|unsat)' comment_char = ';' - elif benchmark_ext == '.cvc': - pass elif benchmark_ext == '.p': status_regex = r'% Status\s*:\s*(Theorem|Unsatisfiable|CounterSatisfiable|Satisfiable)' status_to_output = lambda s: '% SZS status {} for {}'.format( @@ -215,7 +213,7 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, check_unsat_cores = False check_proofs = False else: - sys.exit('"{}" must be *.cvc or *.smt or *.smt2 or *.p or *.sy'.format( + sys.exit('"{}" must be *.smt2 or *.p or *.sy'.format( benchmark_basename)) benchmark_lines = None @@ -331,13 +329,12 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code, '--check-synth-sol' not in all_args: all_args += ['--check-synth-sol'] if ('sat' in expected_output_lines or \ - 'not_entailed' in expected_output_lines or \ 'unknown' in expected_output_lines) and \ '--no-debug-check-models' not in all_args and \ '--no-check-models' not in all_args and \ '--debug-check-models' not in all_args: extra_command_line_args += ['--debug-check-models'] - if 'unsat' in expected_output_lines or 'entailed' in expected_output_lines: + if 'unsat' in expected_output_lines in expected_output_lines: if check_unsat_cores and \ '--no-produce-unsat-cores' not in all_args and \ '--no-check-unsat-cores' not in all_args and \ |