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.

diff --git a/test/regress/regress0/simple-uf.smt b/test/regress/regress0/simple-uf.smt
index 9611a6d799aede40e3d0562f71194885b9be12c7..0a17533315d71ed0f4f9128746b8c114a420aac5 100644 (file)
--- 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 59913a9d63d7af81431a3ff06b1fa56fedf6ecb3..8918c75c1dc6ff005f96b77dcf5b8e76ac7c8120 100755 (executable)
--- 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.