[SMT-COMP] about to start the competition - information and actions for competitors

[David Cok]

Non-competitors: The relevant piece of information for you is that 
progress will be available at 
smtcomp.sourceforge.net/2014/results-toc.shtml (these pages will be 
improved as well as updated with progress as the competition proceeds).

SMTCOMP competitors:

Thanks for all of the work - some late last night - to get all the 
solvers in. Here is some information and some things for you to do.

1) I tried to carefully sort through the flood of email, but I may have 
missed something. So check the entries for your solvers on the 
participants web page - be sure I have recorded the correct solver and 
configuration (and divisions). If there are any typos in names etc. feel 
free to point them out as well.

2) You now have time to complete a solver description, if you have not 
already sent me one. If there is a ? in the column for solver 
description on the participants table, I don't have one from you (or I 
don't know that I have it).

3) I have given the competitors permission to see the submitted solvers 
and the competition space.  It is under
"Competitions and Evaluations"/SMTCOMP2014/Competition and "Competitions 
and Evaluations"/SMTCOMP2014/Solvers . Don't change anything there, if 
by mistake you have permission to do so. If you can't see it, let me know.

4) You will note that the competition is divided into heats. We are 
unsure of how long the computations will take, in part because we have 
many new submissions. So we will do 1000 benchmarks for each division 
first (if there are that many), and then the next 1000, etc. Each heat 
was chosen according to the rules from any benchmarks left after 
previous heats have been removed. We will progress all divisions 
equally, with the exception that we will attempt to complete all 
benchmarks of QF_BV. If the competition ends with some heats for some 
divisions not completed, no data from the uncompleted heats will be used.

5) Because of the heats and the many divisions, StarExec does not give 
an easy overall view of the competition's progress. We have put together 
some web pages summarizing the status. These will be refreshed as the 
competition progresses (around the clock, once I find a place other than 
my laptop to do the computations). You may have to empty the cache on 
your browser regularly to see the progress. The progress page is linked 
off the smtcomp website at
smtcomp.sourceforge.net/2014/results-toc.shtml .

6) We will use a timeout of 40 minutes wall and cpu time per benchmark. 
Some of our estimates suggest that we could extend beyond this, but we 
are unsure of how much overhead time there will be, or restarts, or our 
own fumbling with StarExec.

7) We are still working through recusing the benchmarks that depend on 
the semantics of divide-by-zero, per the earlier discussion. We may 
start the competition jobs anyway and remove the benchmarks at issue 
after the fact.

8) We had two withdrawals, because of bugs that could not be fixed in 
time. If those solvers are submitted late, we will accept them as 
non-competitive entries. The same is true for any currently entered 
solver that is resubmitted because of a bug found during competition.

9) As previously stated, we will attend to the application track once we 
have the main track underway. More about that later.

10) If you see something amiss, by all means email.

The organizers.