[SMT-LIB] A few more SMT-LIB benchmark updates

Morgan Deters mdeters at cs.nyu.edu
Fri Jun 18 02:58:36 EDT 2010


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 in 26 QF_BV benchmarks that have been
reported over the last few days.

The list of changed benchmarks follows.  Also, 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-18

These benchmarks will also be available on SMT-Exec shortly (within an
hour or so) as benchmark revision '20090618-smtlib2'.

Specifically, today's release:

   * fixes the quoting of some benchmarks' :source information attributes
   * fixes the symbol-handling assumptions of
     QF_BV/check2/symbols.smt2 in accordance with a recent
     clarification on the SMT-LIB mailing list, and
   * slightly adjusts the QF_BV/check2/bvnor.smt2 benchmark for
     consistency (without any substantial changes).

The changed benchmarks are:

   QF_BV brummayerbiere/nextpoweroftwo016.smt2
   QF_BV brummayerbiere/nextpoweroftwo032.smt2
   QF_BV brummayerbiere/nextpoweroftwo064.smt2
   QF_BV brummayerbiere/nextpoweroftwo128.smt2
   QF_BV brummayerbiere/nextpoweroftwo256.smt2
   QF_BV brummayerbiere/nextpoweroftwo512.smt2
   QF_BV brummayerbiere3/maxor008.smt2
   QF_BV brummayerbiere3/maxor016.smt2
   QF_BV brummayerbiere3/maxor032.smt2
   QF_BV brummayerbiere3/maxor064.smt2
   QF_BV brummayerbiere3/maxor128.smt2
   QF_BV brummayerbiere3/maxor256.smt2
   QF_BV brummayerbiere3/minor008.smt2
   QF_BV brummayerbiere3/minor016.smt2
   QF_BV brummayerbiere3/minor032.smt2
   QF_BV brummayerbiere3/minor064.smt2
   QF_BV brummayerbiere3/minor128.smt2
   QF_BV brummayerbiere3/minor256.smt2
   QF_BV brummayerbiere3/minxorminand008.smt2
   QF_BV brummayerbiere3/minxorminand016.smt2
   QF_BV brummayerbiere3/minxorminand032.smt2
   QF_BV brummayerbiere3/minxorminand064.smt2
   QF_BV brummayerbiere3/minxorminand128.smt2
   QF_BV brummayerbiere3/minxorminand256.smt2
   QF_BV check2/bvnor.smt2
   QF_BV check2/symbols.smt2

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


More information about the SMT-LIB mailing list