[SMT-COMP] about to start the competition - information and actions for competitors
David Cok
dcok at grammatech.com
Mon Jun 16 12:53:08 EDT 2014
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.
More information about the SMT-COMP
mailing list