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

[Morgan Deters]

Hi everyone,

I've been rolling out fixes over the last week to numerous benchmarks
as problem reports have come in.  All known issues have now been
resolved, with the exception of some of the problems with syntactic
linearity restrictions raised on the mailing list by David Cok this
morning (these should be fixed by tomorrow).  All fixes are available
via the rsync interface as well as the web interface.  A changelog
summary is available on the benchmark page; a more detailed summary
appears below, including acknowledgments.

I especially want to thank David Cok for his efforts developing the
jSMTLIB tool, which I've used, where possible, to test benchmark
compliance.

If you used rsync previously, you can simply use it again to update
your directory with any revisions to that (subset) of benchmarks.  If
you used the web interface, you will need to re-download any affected
benchmarks; you can use the query "modified > 2011-05-15" to narrow
the view to _only_ those benchmarks that have been modified since the
last announced release.

Details of recent changes:

* Incorrect (set-info...) in QF_BV/asp/DisjunctiveScheduling
benchmarks fixed. (Thanks, Leonardo de Moura.)

* Improper real literals in mixed real-integer benchmarks, e.g. the
use "(log 330)" where log is "(Real) Real".  This had been previously
fixed in CVC3's benchmark translator and in the benchmarks, but old
translations were included in the releases; rechecking then raised
additional, related issues.  All is now fixed.  (Thanks, Tjark Weber,
for the report.)

* Several benchmarks in QF_BV/sage/app7 were truncated during
translation.  Fixed.  (Thanks, Tjark Weber.)

* Some check benchmarks in QF_UFIDL and QF_UFLIA were labeled with the
logics "QF_IDL" and "QF_LIA".  Indeed, these check benchmarks don't
include uninterpreted functions, though in these cases they should be
labeled with the logic they are categorized under.  Fixed.  (Thanks,
Tjark Weber.)

* QF_UFNRA/cas benchmarks were missing content.  This is fixed.
(Thanks, Tjark Weber.)

* Numerous fixes to the QF_BV/mcm and QF_NIA/mcm benchmarks:
improperly-typed define-funs, incorrect unary applications of
"(or...)", and removed the benchmark "QF_NIA/mcm/187.smt2", which was
malformed.  (Thanks, David Cok, Tjark Weber, and Nuno Lopes, for each
providing reports of distinct issues in these benchmarks.)

* Improper placement of some QF_AUFBV/stp benchmarks' set-logic commands fixed.

In addition, a fix has been applied to the benchmark downloading
mechanism where sometimes a symbolic link would appear in the custom,
downloaded tarball, in place of the actual benchmark.  (Thanks, Nuno
Lopes.)

Morgan
-- 
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/