[SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[Tjark Weber]

Zhoulai,

On Fri, 2016-05-13 at 13:26 +0800, Zhoulai Fu wrote:

> I find that Alberto Griggio proposed >200 benchmarks for the SMT-COMP
> 15'QF_FP division, but for some reason they were not used in the final
> competition.    Would you let me know whether those benchmarks will be
> used in this year's competition?  In fact,  since the other 2015's
> QF_FP benchmarks  mostly consist in sanity checks (e.g. "x==1e-242 /\
> y == 1e-197") only and can even be solved via a quick syntax analysis
> I guess, will you add more challenging floating-point benchmarks such
> as Griggio's for SMT-COMP 2016?  Thanks for your help.

If I remember correctly, Griggio's benchmarks were ineligible for the
competition because their satisfiability status was unknown. I do not
think that this has changed until now.

Ideally, we (or the SMT-LIB maintainers) would make an attempt to
determine the status of these benchmarks, and then include them in the
competition. However, I am not very confident that there will be enough
time to do this before the benchmark freeze for 2016.

Best,
Tjark