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

[Tjark Weber]

Morgan,

Thanks for this new benchmark release!

On Mon, 2011-05-16 at 00:25 -0400, Morgan Deters wrote:
> * 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.

This issue seems to persist in numerous benchmarks.  For instance,
AUFLIRA/nasa/fol_simplify_arithmetics/gauss_init_0265.fof.smt2 applies
'log' (of type (Real) Real) to '330'.  If my parser is correct, as many
as 1415 benchmarks in AUF{L,N}IRA may still be affected.

It seems that benchmark QF_BV/sage/app7/bench_1436.smt2 was accidentally
truncated.  The benchmark has no assertions, no (check-sat) and no
(exit) command.

Four benchmarks (namely QF_UFIDL/check/bignum_idl1.smt2,
QF_UFIDL/check/int_incompleteness1.smt2, QF_UFLIA/check/bignum_lia1.smt2
and QF_UFLIA/check/bignum_lia2.smt2) (correctly) set a logic that is
less general than their classification, e.g., QF_IDL instead of
QF_UFIDL.

Kind regards,
Tjark