[SMT-COMP] SMT-COMP 2007 -- call for suggestions

[Albert Oliveras Llunell]

Dear colleagues,

As you probably know, SMT-COMP'07 will take place next July in
collocation with CAV at Berlin. As was done last year, before
posting the official rules for this edition we would like to receive
as many suggestions as possible from participants and other people
interested in the event. We will collect suggestions until March 18,
at which point we will start defining the rules for the next edition.

Although all suggestions are welcome, here we outline some potentially
interesting topics:

- Requirements for a solver to enter the competition: an interesting
point concerns the submission of solvers that, after some
preprocessing, call other SMT solvers. Last year's policy was that
an SMT solver could be used in this fashion only if it was from last
year's edition and permission was given by the authors of the solver.

- Technical setting of the competition: number of benchmarks executed,
time given for benchmark, distribution among industrial / crafted
/random benchmarks, punctuation system, disqualification policy,
addition/deletion of a division, scrambling, ...

- Organizational details: format of the presentation session at
SMT'2007, awards (to solvers and maybe even to benchmark submissions,
as is done in the SAT competition), timeline, display of real-time
results, ....


Best wishes,
Albert, for Aaron and Clark too.