[SMT-COMP] Call For Benchmarks

[Jochen Hoenicke]

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
2021 competition is *March 15, 2021*.

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', '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'

If you have large complex benchmarks that are important to you and unsolved
within some reasonable time limit, we are especially interested to see
them. We plan to have a parallel and a cloud track where solvers can use
the combined power of multiple cores or machines to solve a single
benchmark.  We would particularly like benchmarks that come with a
description of why they are difficult and important.  Of course, new
challenging benchmarks are always appreciated.

In your submission please 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 (chair), Albert-Ludwigs-Universität Freiburg, Germany
Antti Hyvärinen, Università della Svizzera italiana, Switzerland