[SMT-COMP] SMT-COMP'20 call for benchmarks

[Antti Hyvärinen]

CALL FOR BENCHMARKS:

Have interesting or hard benchmarks that can be made public? Want the
world’s best SMT solvers to compete to solve *your* problems? Submit
your benchmarks to SMT-LIB and SMT-COMP!

Please let us know as soon as possible if you are considering submitting
benchmarks, even if the material is not quite ready. We will work in
close cooperation with the SMT-LIB maintainers to integrate such
benchmarks into SMT-LIB. The deadline for submission of new benchmarks
to be used in the 2020 competition is * March 1st, 2020. *

We encourage new benchmarks in the following logics (which appear to
have ‘stagnated’ in the sense that the benchmarks in them are no longer
challenging to competitive solvers):

'ALIA', 'AUFLIA', 'AUFNIRA', 'NIA', 'NRA', 'QF_ANIA', 'QF_AUFBV',
'QF_AUFNIA', 'QF_DT', 'QF_FP', 'QF_LIRA', 'QF_NIRA', 'QF_RDL',
'QF_UFBV', 'QF_UFIDL', 'QF_UFLIA', 'QF_UFLRA', 'QF_UFNIA', 'QF_UFNRA',
'UFBV', 'UFIDL', 'UFLRA'

We especially solicit submissions to the Industrial Challenge Track
introduced last year.  These are new difficult benchmarks that are
important to you and either unsolved, or unsolved within some reasonable
time limit. We would particularly like benchmarks that come with a
description of why they are difficult/important.  Of course, if this is
not possible then new challenging benchmarks are always appreciated.
Also, unless we receive a substantial number of new benchmarks, we will
not run the Industrial Challenge Track in 2020.

In your submission pease follow the guidelines in
https://smt-comp.github.io/benchmark_submission.html.

Sincerely,

The organizing team

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