[SMT-COMP] SMT benchmarks for SuperOptimization

[Giles Reger]

Hi Paulo,

> I wanted to submit some benchmarks last year generated by my
> superoptimizer S10 (https://linki.tools/s10). Unfortunately I missed the
> deadline last year.
> 
> This year everything looks ready enough to proceed.
> 
> So, a few questions (these are QF_BV benchmarks):
> 
> - I have the benchmarks written in SMT2 format. Some of them are are
> quite hard (as in take > 12hours). I assume these should not be
> included, right?

The SMT-LIB and SMT-COMP projects are distinct but (obviously) closely related. SMT-LIB is used for much more than just running the competition and I think it is of general benefit to the community to submit non-trivial benchmarks to the library.

This year we have the “industry challenge” track where we will run on fewer benchmarks for much longer time limits. Your difficult benchmarks may be relevant here. For this track we ask that you also submit a separate description of why the benchmarks are interesting.

In summary, I would encourage you to also submit these “quite hard” benchmarks.

> - Shall I choose benchmarks taking only less than 1hr or 40 mins (the
> smtcomp time)?

My above comments would apply here. If you have a lot of similar benchmarks it is helpful if you are able to trim them down in a way that preserves ‘diversity’ (in terms of difficulty etc) although we appreciate that this is difficult.

> - Do I need to add to these benchmarks the known benchmark status?
> (sat/unsat)

If you are confident in the status then please do add it. The SMT-LIB people do run checks to fill in missing statuses but it is useful to add them if you know them. Benchmarks with unknown status are treated differently in the competition (but still included) with respect to negative scoring.

> - Anything else I need to do?

Further details on what you have to do to submit benchmarks to SMT-LIB can be found here:

https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending

Thanks and best wishes,
Giles

> -- 
> Paulo Matos
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp