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

[cok at frontiernet.net]

Regarding constructions like (log 330) in AUFLIRA and AUFNIRA.

Both those logics contain language describing implicit conversion of Int to Real
in binary functions that have one Int and one Real argument. There is also the special
case of / in which both arguments may be implicitly converted. No implicit conversions
happen anywhere else. Do I recall that implicit conversions were deprecated?  Or do we
really prefer having just these special cases.

- David

----- "Morgan Deters" <mdeters at cs.nyu.edu> wrote:

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