[SMT-COMP] SMT-COMP 2019: Call for Comments, Benchmarks, Solvers

[Mathias Preiner]

Tjark,

On 1/31/19 1:29 PM, Tjark Weber wrote:
> Note that this argument applies also to benchmarks that are "too hard."
> Running a hard benchmark only to find that every solver timed out is,
> in a sense, not very useful either. (In fact, it is worse: it probably
> takes as long as running hundreds of trivial benchmarks.)

I disagree. The SMT-COMP organizers plan to filter out easy benchmarks
based on the results of the previous competition. However, they can't
foresee if solvers will be able to solve hard benchmarks in the next
competition. As solver developer you focus on benchmarks that have not
been solved in the past.

Cheers,
Mathias



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190131/cd274c6c/attachment.asc>