[SMT-COMP] SMT-COMP'09 extended to include extra divisions

[Morgan Deters]

Hello SMT-COMPers,

We have found and catalogued a number of new benchmarks recently, and
have recategorized some others.  Accordingly, we are announcing the
extension of SMT-COMP 2009 to include several additional theories.  As
you'll note, many of the newly-collected benchmarks depend on
non-linear real and integer arithmetic, and this will be the first
time such benchmarks are included in SMT-COMP.

  LRA
  QF_NIA
  QF_UFNRA
  UFNIA
  AUFNIRA

For each (combined) theory, should two or more solvers be submitted to
SMT-COMP that can handle it, we'll run it as an SMT-COMP division.
Should only one solver be submitted that can handle the division,
we'll run it _after_ the main competition as an "SMT Exhibition."
While not officially part of SMT-COMP, such an exhibition will have
the same visibility during CADE as the rest of SMT-COMP---assuming
that the conference doesn't end before such exhibition does.
Naturally, as organizers, our focus has to be on the official
SMT-COMP.

Of course, it will be mentioned during the SMT-COMP session of CADE
that these divisions were added late in the competition season, and
that tools able to solve any of these benchmarks demonstrate
improvement over the tools submitted to SMT-COMP last year.

The benchmarks in these divisions are already available on the SMT-LIB
website:

   http://combination.cs.uiowa.edu/smtlib/

...and will soon be available for execution on SMT-Exec under the
benchmark revision "20090702" (the date of the most recent SMT-LIB
release):

   http://www.smtexec.org/

Regards, and see you next month,
Morgan (also for Aaron, Albert, and Clark)
-- 
Morgan Deters
mdeters at lsi.upc.edu