Wrongly Classified Benchmarks

8 views
Skip to first unread message

Jochen Hoenicke

unread,
Jun 30, 2021, 10:06:50 AM6/30/21
to smt...@googlegroups.com, smt-...@cs.nyu.edu
Hello all,

When analyzing the SMT-COMP results we found benchmarks that do not
fit in their corresponding logic in the latest SMT-LIB release.

There are several thousand benchmarks in linear arithmetic using div,
mod, or non-linear arithmetic. We will remove these benchmarks from
the scoring, since they do not conform to their logic. Here are the
number of problematic benchmarks by logic:

AUFBVDTLIA: 7
AUFDTLIRA: 1096
AUFFPDTLIRA: 21
LIA: 191
QF_SLIA: 65
UFDTLIRA: 2581
UFFPDTLIRA: 10

Roughly half of these benchmarks were selected in the competition.

Also there are 168 benchmarks in the logics *FP that use to_fp with a
real number as argument, which are only allowed in the *FPLRA logics.
Half of them are in the incremental track. We plan to remove these
from the scoring as well.

There are 44 benchmarks in QF_SLIA that contain quantifiers and that
we plan to remove from the scoring.

Moreover, there is a whole new family of benchmarks in NRA
(20200911-Pine) that doesn't use quantifiers, but are not classified
as quantifier-free. While this is clearly not intended, we plan to
still keep these benchmarks in the scoring, since they are valid
benchmarks.

A full list of benchmarks is available at
https://smt-comp.github.io/2021/excluded_benchmarks/SMT-LIB_excluded.tar.xz

Regards,
The organizing team
Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil
Jochen Hoenicke (chair), Albert-Ludwigs-Universität Freiburg, Germany
Antti Hyvärinen, Università della Svizzera italiana, Switzerland

Mathias Preiner

unread,
Jul 15, 2021, 1:46:48 PM7/15/21
to smt...@googlegroups.com
Hi Jochen,

Thanks for pointing out the misclassified benchmarks.

We'll will fix the issues for the next SMT-LIB release.

Cheers,
Mathias
OpenPGP_0xA4AF2BDE778B2463.asc
OpenPGP_signature
Reply all
Reply to author
Forward
0 new messages