From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Sun, 4 Aug 2019 07:04:20 +0000 (-0700)
Subject: Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)
X-Git-Tag: cvc5-1.0.0~4044
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3070131bace10028498003c2f6cfd6f40a50358;p=cvc5.git

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 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.