Re: [Smtcomp-discussion] SMT-LIB benchmarks and SMT-COMP 2015

[Clark B. <ba...@cs...>]

David,

I have been maintaining the official SMT-LIB benchmark library.
Currently, the most recent copy is on StarExec.

There is one major update pending: we need to update the status of
many of the "unknown" benchmarks based on a run David Cok did last
summer.  I hope to be able to complete this before May 1.

Otherwise, for new benchmarks, the typical approach is to run them
with a large timeout through several solvers (the competition solvers
from last year, say) to determine well-formedness and status.  If at
least two solvers agree on their status, we typically accept that as
the status.  Otherwise, the status is unknown.  Sometimes the
benchmark providers know the status for one reason or another.
Whenever possible, we ask them to provide the status.

My suggestion would be to follow the above process for any newly
submitted benchmarks and then contact me to upload the benchmarks once
you have verified that things look good.

We are in the process of developing a special-purpose tool for
checking well-formedness of bechmarks, but I don't know if it will be
ready before May 1.

-Clark


On Mon, Mar 16, 2015 at 5:25 AM, David Deharbe <da...@di...> wrote:
> Dear Coordinators of the SMT-LIB and Maintainer of the SMT-LIB Benchmarks Repository,
>
> As a responsible for handling the submissions of benchmarks for the 2015 edition of SMT-COMP, I am contacting you to obtain informations on the procedure to get new benchmarks to the SMT-LIB repository. In particular, I would like to know if there is an official tool to check well-formedness of the benchmarks, and a standard way to decide the status of the benchmarks.
>
> We (the SMT-COMP organisers) have established May 1st as deadline for benchmark submissions. We would like to handle such submissions as early as possible so that any problem that may happen can be solved and have as wide a variety of benchmarks as possible for the next edition of our contest.
>
> Best regards,
>
> — David.