[SMT-COMP] SMT-COMP 2016: Benchmarks in 2.0 and 2.5 Formats

[Tjark Weber]

Dejan,

On Thu, 2016-05-26 at 17:47 +0000, Dejan Jovanović wrote:
> Can you please give the final word on this. Will only the "known"
> benchmarks be used in the competition?

Yes. The competition rules are quite clear that benchmarks with unknown
status will not be used. This has been established practice of SMT-COMP 
for a long time, and as mentioned earlier, I do not believe it would be
appropriate to change this on short notice. The implications of such a
change for the size of the competition, for the competition tools and
its scoring rules are non-trivial and deserve careful consideration.

Of course, the performance of solvers on benchmarks with unknown status
is still of interest. If there is sufficient time after we've run the
competition jobs, we may make an attempt to determine it and report our
findings at the SMT Workshop in addition to the competition results.

If I am involved in organizing SMT-COMP again in 2017, I would aim to
incorporate benchmarks with unknown status in a more systematic manner
then.

Best,
Tjark