[SMT-COMP] dual-core for SMT-COMP 2010?

[Aaron Stump]

Dear SMT-COMP community,

I'm writing to ask your opinion about whether or not we should enable the
dual-core feature of our cluster (www.smtexec.org) for SMT-COMP 2010. The
cluster machines all have dual cores, but we have disabled the use of the
second core in all previous competitions. The motivation for enabling it, of
course, is to incentivize solver implementors to add some support for
concurrency to their tools. This could lead to significant benefits for the
applications that use SMT solvers. As the SMT field has matured over the
past five years or so, it seems time to take this next step, to encourage
and reward concurrent implementations. This does, of course, impose an
additional burden on solvers (particularly new ones) entering the
competition. My personal feeling is that we ought to accept this burden and
enable the dual core feature, for the benefit of our applications, and also
for the respect of the field: the multicore revolution has been underway for
quite some time, and we should officially join it as soon as possible.

Please let us know what you think (it is fine to reply to this list, and we
can discuss the question here).

Aaron
on behalf of the SMT-COMP 2010 organizers (Clark Barrett, Morgan Deters,
Albert Oliveras, Aaron Stump)