[SMT-LIB] Updated SMT-LIB released

[Morgan Deters]

Hi SMT-LIB and SMT-COMP communities,

There is a new benchmark release of SMT-LIB available at

  http://www.smtlib.org/

that fixes some problems with the library that were reported to us,
and introduces some new benchmarks.

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

   modified >= 2010-06-15

Specifically, today's release moves some benchmarks to properly
represent their logic, and also fixes incorrect (set-logic...)
commands in some benchmarks.

  Some benchmarks moved from UFNIA/spec_sharp to AUFLIA/spec_sharp
  Some benchmarks moved from AUFLIRA/why to AUFNIRA/why
  Incorrect (set-logic ...) fixed in benchmarks in QF_AUFLIA/check
  Incorrect (set-logic ...) fixed in benchmarks in QF_LRA/miplib
  Incorrect (set-logic ...) fixed in benchmarks in QF_UFLRA/mathsat
  UFLRA benchmarks from AUFLIRA/misc moved to UFLRA/misc

In addition, the QF_LRA/miplib and QF_UFLRA/mathsat benchmarks were
adjusted slightly so that they conform to the strict SMT-LIB
definition of "linear."

Also, this release includes contributions in QF_RDL, QF_LRA, QF_LIA,
QF_NRA, QF_BV, QF_UFBV, and QF_AUFBV, from:

Alberto Griggio:
  QF_LIA/CAV_2009_benchmarks
  QF_LIA/convert (resulting from image conversion)
  QF_LIA/cut_lemmas (crafted benchmarks)
  QF_LIA/rings_preprocessed (crafted benchmarks)

Ivan Jager:
  QF_AUFBV/check (simple checking of encodings)
  QF_BV/stp_samples
  QF_BV/dwp_formulas
  QF_AUFBV/stp_samples
  QF_AUFBV/dwp_formulas

Fred Maris:
  QF_LRA/DTP-Scheduling (planning)
  QF_RDL/SMT-Temporal-Planning-Benchmarks (from planning: cooking)

Trevor Hansen:
  QF_BV/check2 (simple conformance-checking for SMT-LIB format v2)

Harald Roman Zankl:
  QF_NRA/zankl (termination of term rewriting)

Bryan Brady:
  QF_BV/pipe (Burch and Dill style correspondence checking on a simple toy processor)
  QF_AUFBV/pipe
  QF_AUFBV/btfnt (a variant of the Y86 processor described in Bryant's textbook)
  QF_UFBV/btfnt
  QF_AUFBV/calc2 (arising from a calculator example from IBM)
  QF_UFBV/calc2

A special thanks to submitters of the new benchmarks.

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