[SMT-COMP] Scoring rules in the draft SMT-COMP 2015 rules

Tjark Weber tjark.weber at it.uu.se
Tue May 12 10:29:16 EDT 2015


David,

On Mon, 2015-05-11 at 22:24 -0400, David R. Cok wrote:
> I note a (minor) change from previous practice in the draft rules for 
> SMTCOMP 2015. In previous competitions the accumulated time used for 
> comparison among solvers was the total of the times for all benchmarks 
> solved correctly. In the 2015 rules, the measured time includes the time 
> taken to produce 'unknown' answers (and wrong answers, though that 
> aspect is likely immaterial).

Thank you for pointing this out. Indeed, I believe this change is both
minor (in the sense that it is unlikely to affect the ranking, except
under very specific circumstances) and desirable. It is now explicitly
mentioned in Section 3 of the rules, as you suggested.

Best,
Tjark




More information about the SMT-COMP mailing list