diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-04 00:04:20 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-04 00:04:20 -0700 |
| commit | d3070131bace10028498003c2f6cfd6f40a50358 (patch) | |
| tree | d95567be644b4660cddd15c851813e43ec3c3932 /test/regress/regress0 | |
| parent | 243a1d58a139077ecf19ac8a68573e51c08e4621 (diff) | |
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.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/simple-uf.smt | 1 |
1 files changed, 0 insertions, 1 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 ) |