[SMT-COMP] SMT-COMP 2020 pre-announcement

[Antti Hyvärinen]

Dear SMT-COMP participants, dear SMT-LIB community,

We were happy to be contacted by the SMT steering committee to
organise the international SMT competition 2020.  The steering
committee specifically tasked us with finding ways of making the 2020
competition lighter to run in comparison to the previous editions and
in particular that of 2019.

To achieve the goal while keeping the quality of the competition high,
we are suggesting the following changes:

1. Reducing the number of benchmarks to run in each division.  This
was already done in 2019 with a formula that resulted in 50% of
benchmarks being run in bigger divisions.  We plan to further decrease
this percentage to 40% in 2020.

2. Reducing the number of submissions per team per track: We plan to
allow a single solver per track for each solver development team.

3. Reducing the timeout.  In 2020 the timeout was set to 40 minutes in
the single-query track.  We plan to decrease this to 20 minutes in all
tracks.

4. Moving the solver submission deadline further away from the
workshop by two weeks.  This would put the deadline for the first
versions of the solvers roughly to the beginning of May 2020.

5. Changing the rules so that text printed to standard error will not
be ignored but will be combined together with standard output.

The motivation for these changes is as follows.  Based on the data
from 2019, with the changes 1 and 2 in place, the number of jobs run
for the competition would have dropped roughly by 40% (from 781'659 to
496'715).  In case that SMT-LIB grows significantly in 2020, we might
consider a lower percentage (while, as in 2019, favouring the new
benchmarks). Reducing the timeout and moving the solver submission
deadline makes re-running divisions in case of problems less stressful
for the organisers.  The reason for joining the standard input and
standard error is related to StarExec, and removes a possible source
of error where the change would have to be done manually by the
organisers.

We hope that these changes will have a two-fold positive effect on the
competition: keep the quality of the competition high; and allow
further development of the competition concept by giving more time to
the current and future organisers for planning for improvements.

We would be happy to receive community's feedback on the suggestions!

Best regards,

Haniel Barbosa, Jochen Hoenicke, and Antti Hyvärinen (chair)