[SMT-LIB] Final Benchmarks

[Clark Barrett]

Greetings to the SMT-COMP and SMT-LIB communities.  As you know, we have been
working on finalizing the new bitvector theories for a while.  I am happy to
report that the new theories and logics have now been posted on the smtlib web
site.  They are very similar to the last draft I circulated on these lists, the
only changes being a correction to the definition of bvashr and removal of a
copule of the more obscure operators.

I am also happy to report on the successful translation of over 8000 benchmarks
into the new QF_BV and QF_AUFBV logic formats.  I was hoping to get these done
sooner, but as you can imagine, getting that many benchmarks translated is
quite challenging (there are always unexpected problems).

Curiously, we actually have no benchmarks in the QF_UFBV category.  The
benchmarks from last year have been retranslated and they all landed either in
QF_BV or QF_AUFBV.

Currently the plan for the competition is to have two bitvector divisions
(QF_BV and QF_AUFBV) and to use all the benchmarks in QF_BV and QF_AUFBV.
Since this will require changes to parsers and algorithms, let me know now if
anyone has a big problem with this.  The format has been available for some
time, so hopefully you've already started making the necessary modifications.

This also represents the last changes to the benchmarks before the competition
(modulo any errors that are found).

Happy benchmarking!

-Clark