From d3070131bace10028498003c2f6cfd6f40a50358 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Sun, 4 Aug 2019 00:04:20 -0700 Subject: [PATCH] Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155) The regression script did not extract the expected status from incremental SMT-LIB v2 benchmarks correctly if status was given via (set-info :status ...). The script used re.search for finding the status, which only searches for the first occurrence instead of finding all (set-info :status ...). This commit fixes the issue by using re.findall instead. --- test/regress/regress0/simple-uf.smt | 1 - test/regress/run_regression.py | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/test/regress/regress0/simple-uf.smt b/test/regress/regress0/simple-uf.smt index 9611a6d79..0a1753331 100644 --- a/test/regress/regress0/simple-uf.smt +++ b/test/regress/regress0/simple-uf.smt @@ -4,5 +4,4 @@ :extrasorts (A B) :extrafuns ((f A B) (x A) (y A)) :formula (not (implies (= x y) (= (f x) (f y)))) - :status unsat ) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index 59913a9d6..8918c75c1 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -213,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. -- 2.30.2