[SMT-LIB] SMT-COMP update

[Alberto Griggio]

Dear list,

I'm sorry that we need another update email, but we have just realized
that we need one more fix (hopefully, the last one).

> - Fixed some conformance issues and translation bugs in the
>  "kind_QF_UFIDL" benchmark sets. In particular:

We have just realized that the "kind" set of benchmarks was
misclassified as QF_UFIDL, where in fact the original benchmarks were
meant to be in QF_UFLIA (or in QF_UFLIRA in some cases, but we already
removed all the rational constants and functions -- see the previous
update email).

Since nobody had noticed the problem before, we assume that people have
been testing these benchmarks with SMT solvers supporting a larger logic
than QF_UFIDL. Therefore, we have decided that for SMT-COMP'11 we will
reclassify all the "kind" benchmarks as QF_UFLIA. After SMT-COMP, we
will probably perform a more fine-grained classification of such
benchmarks, in order to distinguish those that are in the QF_UFIDL
fragment, and to re-introduce those using rational constants and
functions as QF_UFLIRA.

We hope this reclassification will not cause problems. However, we
believe this is the safest option at this stage.


The SMTCOMP'11 Organizers
Roberto, Morgan, and Alberto