[SMT-LIB] Updates for SMTCOMP 2012

[cok at frontiernet.net]

Dear SMTCOMP participants and onlookers,

SUMMARY:
- updated information (rules, list of eligible benchmarks) are available from the web-site: www.smtcomp.org/2012
- solver registrations are due on 15 June.


DETAIL:

In preparation for SMT-COMP 2012, we have updated the information about
benchmark statuses (for many of the unknown ones) and difficulties.
The information is available from the SMTCOMP website. In particular, there
are two files, in the format accepted by the benchmark selection tool
available from http://www.smtcomp.org/2012/tools.shtml

The first file, smtlib2012-benchs.txt, contains information about all
the benchmarks that are currently part of SMT-LIB. 

The second file, smtcomp2012-eligible.txt, contains only the benchmarks
that will be eligible for SMT-COMP 2012, according to the rules. This
differs from the above not only because benchmarks in divisions that
will not be part of the competition have been removed (e.g. QF_UF,
QF_AX, ...), but also because some benchmark divisions include benchmarks
from subsumed divisions, as described
in the rules. 

In both cases, the new statuses and difficulties have been computed by
running last year's competitors on SMT-Exec. The jobs used for this are
public:

   http://www.smtexec.org/exec/?jobs=930
   http://www.smtexec.org/exec/?jobs=962
   http://www.smtexec.org/exec/?jobs=970

In case you haven't noticed yet, new application track benchmarks are
available from http://smtcomp.sourceforge.net/2012/application.shtml,
together with benchmarks for the unsat core track.

We have also slightly updated the scrambler: it is the same as last
year, except that it has been extended to support the unsat core track:

- using the option "-scramble_named_annot true", also :named annotations
  will be scrambled

- using the option "-core FILE", where FILE is the output produced by a
  SMT-LIB2 compliant solver, it is possible to generate a "core file" of
  the input benchmark, i.e. a benchmark containing only the assertions
  in the unsat core produced by a solver. This will be used for checking
  the correctness of the results produced by solvers in the unsat core
  track. For instance, if the benchmark "test.smt2" contains 5
  assertions named A1 ... A5, and a solver produces the following
  output (in a file called "output.txt"):
      
    unsat
    (A3 A2 A5)

  then using:

    ./scrambler -core output.txt < test.smt2 > core.smt2

  it is possible to generate the corresponding core file.


Finally, we remind you that the deadline for submitting the solvers is
in two weeks (June 15). For any questions, comments, or other kind of
feedback, do not hesitate to contact us.


Best,
  David, Roberto and Alberto