[SMT-LIB] QF_UFBV: on last-minute extension with sign

[Alessandro Cimatti]

Dear colleagues,

first, I would like to thank Clark and all the people involved in the
preparation of the benchmarks for the QF_UFBV32 cathegory. It has
surely been a lot of work!

However, I think that the extension of QF_UFBV32 with signed operators
should not be accepted at this stage of the competition.

In fact, the bit vectors theory has been fixed a long time ago --- the
description was posted on the list by Cesare on May 5th.  The
description made it clear that the interpretation would be
unsigned. That signed arithmetic would not be part of the theory had
been discussed and agreed upon with Cesare, Silvio, and others.

No variations were communicated on the topic since. Thus, the
competitors entering this category had no reason to include signed
operators. A last minute addition to the theory would give them a
disadvantage against those who have signed arithmetic operators
already available, or somehow knew that the extension was being taken
into consideration.

Notice that this is really a last minute extension: for the other
categories, not only the theories, but also the benchmarks, have been
frozen more than a week ago.

Besides, it seems that eliminating the signed subset would not be a
big loss.  As far as I can see, the signed operators proposed by Clark
are used only in 437 out of 8247 files. We still have a reasonable
number of instances left for the competition (more than 7800).

As a minor remark, it seems that several benchmarks have undeclared
symbols.  I have not checked pervasively, but it seems that this
problem is rather frequent.

Alessandro