[SMT-COMP] Wrongly Classified Benchmarks

[Jochen Hoenicke]

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