[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions

[Morgan Deters]

Hello everyone,

We have rolled out a new release of SMT-LIB benchmarks this week,
coincident with the May 15 deadline for SMT-COMP 2011 benchmarks.

This benchmark release contains fixed benchmarks, as well as new
benchmarks.  It does *not* include "application track" benchmarks for this
year's competition, which are currently maintained separately from the
SMT-LIB library.

This release is available via the web interface:

   http://www.smtlib.org/

and also via the rsync interface at (for example):

   rsync -az rsync://smtexec.org/smtlib2/QF_UF QF_UF

(You can replace "QF_UF" with other logics, or even leave it off to
download all benchmarks in the library.)

PLEASE NOTE that the entire library is about 71 gigabytes in size, and
that a few select families (QF_BV/asp/DisjunctiveScheduling and
QF_IDL/asp/DisjunctiveScheduling) are a large part of this total; you
may prefer to download the library in parts if you aren't on a fast
connection.

The fixes to existing benchmarks are:

* In AUFLIA (and perhaps others), a sequential-let semantics was
assumed in the translation of certain benchmarks from SMT-LIBv1 to
SMT-LIBv2.  This has been corrected in this release for all affected
benchmarks.
* Certain benchmarks with mixed real and integer arithmetic had
incorrect real literals (e.g. "3" instead of "3.0").  This has been
corrected.  Thanks to Nikolaj Bjorner and Tjark Weber for reporting
this.
* There was a misapplication of quantifier instantiation patterns in
AUFLIA/boogie family (and perhaps others).  This was corrected; thanks
to Jochen Hoenicke for the report.
* Some benchmarks improperly declared symbols "abs" and "mod" even
though the relevant SMT-LIBv2 logic defined these symbols.  Fixed.
Thanks to David Cok for finding this.

New benchmarks in this release are:

* QF_IDL/asp and QF_BV/asp benchmarks from the answer set programming
competition (thanks Ilkka Niemela and Tomi Janhunen)
* QF_BV/rubik Rubik's cube benchmarks (thanks Tim King)
* MCM (multiple constant multiplication) benchmarks in QF_BV/mcm and
QF_NIA/mcm (thanks Nuno Lopes)
* Several families in QF_LIA (dillig, slacks, miplib2003, pb2010,
pidgeons, prime-cone) thanks to Dejan Jovanovic
* Multiplier verification benchmarks QF_BV/uum thanks to Jinpeng Lv

Some benchmarks have more information in the benchmark files
themselves (in the :source informational attribute), or in associated
papers that have been published recently (or will appear shortly).

Apologies if I have forgotten to acknowledge anyone.  Please let me
know if there are any benchmark compliance issues, or if I have
neglected to include a fix, or a benchmark contribution, in this
release.

Thanks,
Morgan
Co-organizer, SMT-COMP 2011 (with Roberto Bruttomesso and Alberto Griggio)

-- 
Morgan Deters
Research Scientist
Courant Institute of Mathematical Sciences
251 Mercer St., New York, NY 10012
mdeters at cs.nyu.edu - http://cs.nyu.edu/~mdeters/