projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 243a1d5) | patch
Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)
authorMathias Preiner <mathias.preiner@gmail.com>
Sun, 4 Aug 2019 07:04:20 +0000 (00:04 -0700)
committerGitHub <noreply@github.com>
Sun, 4 Aug 2019 07:04:20 +0000 (00:04 -0700)
commitd3070131bace10028498003c2f6cfd6f40a50358
treed95567be644b4660cddd15c851813e43ec3c3932tree
parent243a1d58a139077ecf19ac8a68573e51c08e4621commit | 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.
test/regress/regress0/simple-uf.smt diff | blob | history
test/regress/run_regression.py diff | blob | history