[SMT-LIB] Improper unary operators fixed in SMT-LIB

[Morgan Deters]

Hi SMT-LIB and SMT-COMP communities,

We discovered 1500 benchmarks where operators requiring >= 2 arguments
had only one, e.g. (and (= x 10)).  These have been found and
repaired.

Additionally, QF_BV/check2/symbols.smt2 contained a multiply-defined
symbol.  This has been fixed.

Thanks to Alberto Griggio and Florian Lapschies for reporting these
problems initially.

As usual, the benchmarks are available from

   http://www.smtlib.org/

Due to popular demand, we soon intend to have a sync'able repository
of benchmarks available (perhaps via "git").  Hopefully this will ease
the burden of continually re-syncing the benchmark suite.

All changes to the library can be seen (and just these changes
downloaded) by using the SMT-LIB benchmark search interface and
searching for:

   modified >= 2010-06-24

These benchmarks are already available on SMT-Exec as benchmark
revision '20090624-smtlib2'.

These changes affect the following benchmark families:

  QF_BV/gulwani-pldi08
  QF_UF/eq_diamond
  QF_LIA/check
  QF_LIA/bofill-scheduling
  AUFLIA/simplify
  QF_UFIDL/bcnscheduling
  QF_BV/check2

Regards,
Morgan (also for Albert, Clark, Aaron, and Cesare)