[SMT-COMP] status attribute of benchmarks for competition

[Clark Barrett]

Hi SMT-COMP folks,

I have two announcements about the "status" attribute that affect the
competition.

First, it appears that some of the AUFLIA/boogie benchmarks labled as "sat" may
actually be "unsat".  The labelling of these benchmarks was based our best
understanding based on the source application.  However, because of the size
and difficulty of the benchmarks and the inherent incompleteness of all current
approaches to quantifiers, there is no way to be confident that these
benchmarks are really satisfiable.  As a result, we will be relabeling them as
"unknown" which will effectively remove them from the competition.  Note that
there are a few other quantified benchmarks labeled as "sat", but these are
small and we are confident about their status, so we will not be relablling
them.  I would like to suggest that we discuss the problem of how best to
include such benchmarks in future competitions during the meeting at SMT
Workshop this weekend.

Second, we have received several requests from different groups to change the
status of unknown benchmarks based on their own test results.  While we are
very interested in moving as many unknown benchmarks as possible to either
"sat" or "unsat", and do not dispute the correctness of the results submitted
by these groups, we also recognize that such changes before the competition
will essentially make new benchmarks eligible for selection after the benchmark
suite was supposed to be "frozen".  For this reason, after substantial
discussion, we have decided not to make any such status changes before the
competition.  We will make a concerted effort to update the status of as many
benchmarks as possible post-competition.  Again, I would like to suggest that
the issue of how best to confidently assign status attributes be raised during
the discussion this weekend.

-Clark