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

[Antti Hyvärinen]

We are pleased to announce the 2020 edition of SMT-COMP.

SMT-COMP is the annual competition among Satisfiability Modulo Theories
(SMT) solvers.

The goals of SMT-COMP’20 are to encourage scientific advances in the
power and scope of solvers, to stimulate the community to explore and
discuss shared challenges, to promote tools and their usage, to engage
and include new members of the community (in a fun environment) and to
support the SMT-LIB project in its efforts to promote and develop the
SMT-LIB format and collect and collate relevant benchmarks.

The results of SMT-COMP'20 will be announced at the SMT Workshop (July
4-5), which is affiliated with the 10th International Joint Conference
on Automated Reasoning (IJCAR 2020).

This is a call for comments on the changes of the competition rules.

The organizing team is preparing the schedule and rules for 2020.  We
summarise here our proposed changes from 2019.

Any comments you may have on these proposed changes, on how to improve
the competition or to redirect its focus are welcome and will be
considered by the team.  We particularly appreciate comments received
before February 10, 2020.

1. Reducing the number of submissions per team per track.  Solver
   development teams may only submit more than one entry if they are
   substantially different.  A justification must be provided for the
   difference.  We strongly encourage the teams to keep the number of
   solvers per team per category at at most two.  The idea in allowing up
   to two submissions is to encourage the development of new, experimental
   techniques by allowing a “secondary solver” to be submitted, while
   keeping the competition manageable.

2. Disallowing portfolio solvers.  This year we explicitly forbid the
   submission of so-called portfolio solvers as competition entries.  We
   acknowledge that the definition of what constitutes a portfolio
   solver is tricky.  More on this in the call for solver submissions.

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.

6. We will run again the industry challenge track in 2020 given that we
   receive a substantial number of new benchmarks.

7. QF_BV model generation track will no longer be experimental

8. We are planning to have experimental model generation tracks of
   QF_LRA, QF_LIA, QF_IDL, QF_RDL, and QF_LIRA.


COMMUNICATION:

The competition website is at www.smtcomp.org.

The SMT-COMP repository is at https://github.com/smt-comp.

Public email regarding the competition may be sent to
smt-comp at cs.nyu.edu.  Announcements will be sent to both
smt-comp at cs.nyu.edu and smt-announce at googlegroups.com.

SMT-COMP'20 is organized under the direction of the SMT Steering
committee.

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