[SMT-COMP] SMTCOMP news - a provisional Bronze medal winner

[David Cok]

Overnight SMT-COMP 2014 passed the 50% mark.

More significantly the QF_BV division finished, with Boolector in the 
lead as the provisional Bronze medal winner. A new submission by Mate 
Soos based on STP came in second.

I say 'provisional' because when all the data are in hand, we will 
perform some sanity checks to be sure we have counted job results 
properly, run every solver as expected, and that there is no anomalous 
data, duplicate results, missing results, etc. We will also make all the 
data public in a consolidated, convenient form.

At this point most of the divisions are completed, with just 10 still 
computing.

We did have one problem discovered in the past day. One of the solvers 
was 'recycled' in StarExec, causing all job-pairs with that solver to 
fail from that time on. That problem has been corrected (the original, 
submitted solver was retrieved), and those job-pairs have been 
rescheduled for processing.

So a note for all the solvers: I have made StarExec archival copies of 
your solvers. However, all the competition jobs are running with links 
to your original submissions, so I could be sure that I was using the 
correct solver and configuration (by id number). Don't delete or recycle 
those solvers, at least until the competition is officially complete.

Another policy issue arose: one solver on one benchmark  issued a result 
(20 sec) within the timeout period, but did not terminate immediately 
and was recorded with a timeout status. We decided to count this as a 
solved benchmark (not yet reflected in the displayed data). It does not 
make any material change in the results. As a guideline however, we 
suggest that in the future solvers configured for competition terminate 
as promptly as possible (even if messily) after issuing an answer to 
avoid this race condition.

- David