[SMT-COMP] [smt-lib] Call For Benchmarks

[Aina Niemetz]

Hi Nuno,

that would be great!
No lambdas, since they are not standardized.
And yes, maybe filter out those that are solved by Z3 under 1 second.

Also, can you maybe try to group them into families per verification 
task (if that makes sense)?

As for the number of benchmarks.... let's say, a representative and 
interesting set without duplicates?

Aina

On 2/5/21 10:38 AM, 'Nuno Lopes' via SMT-LIB wrote:
> I have plenty of quantified benchmarks using UF+FP+BV+ arrays w/ lambdas 
> (most benchmarks don’t have everything though). These benchmarks are 
> from compiler verification tasks.
> 
> Is this interesting? I can filter out the benchmarks with lambdas if not 
> relevant (don’t know if that’s been standardized or not).
> 
> How many benchmarks would you want? Any filter (e.g., throw away files 
> that are solved by Z3 in under a second)?
> 
> Nuno
> 
> *From:* Jochen Hoenicke
> *Sent:* 05 February 2021 17:26
> *To:* smt-comp at cs.nyu.edu; smt-lib at googlegroups.com
> *Cc:* Antti Hyvärinen <antti.hyvarinen at gmail.com>; Haniel Barbosa 
> <hanielbbarbosa at gmail.com>
> *Subject:* [smt-lib] Call For Benchmarks
> 
> Have interesting or hard benchmarks that can be made public? Want the 
> world’s best SMT solvers to compete to solve /your/ problems? Submit 
> your benchmarks to SMT-LIB and SMT-COMP!
> 
> Please let us know as soon as possible if you are considering submitting 
> benchmarks, even if the material is not quite ready. We will work in 
> close cooperation with the SMT-LIB maintainers to integrate such 
> benchmarks into SMT-LIB. The deadline for submission of new benchmarks 
> to be used in the 2021 competition is *March 15, 2021*.
> 
> We encourage new benchmarks in the following logics (which appear to 
> have ‘stagnated’ in the sense that the benchmarks in them are no longer 
> challenging to competitive solvers):
> 
> 'ALIA', 'AUFNIRA', 'NIA', 'NRA', 'QF_ANIA', 'QF_AUFBV', 'QF_AUFNIA', 
> 'QF_DT', 'QF_FP', 'QF_LIRA', 'QF_NIRA', 'QF_RDL', 'QF_UFBV', 'QF_UFIDL', 
> 'QF_UFLIA', 'QF_UFLRA', 'QF_UFNIA', 'QF_UFNRA', 'UFBV', 'UFIDL', 'UFLRA'
> 
> If you have large complex benchmarks that are important to you and 
> unsolved within some reasonable time limit, we are especially interested 
> to see them. We plan to have a parallel and a cloud track where solvers 
> can use the combined power of multiple cores or machines to solve a 
> single benchmark.  We would particularly like benchmarks that come with 
> a description of why they are difficult and important.  Of course, new 
> challenging benchmarks are always appreciated.
> 
> In your submission please follow the guidelines in
> 
>     https://smt-comp.github.io/benchmark_submission.html
>     <https://smt-comp.github.io/benchmark_submission.html>.
> 
> 
> Sincerely,
> 
> The organizing team
> Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil
> Jochen Hoenicke (chair), Albert-Ludwigs-Universität Freiburg, Germany
> Antti Hyvärinen, Università della Svizzera italiana, Switzerland
> 
> -- 
> You received this message because you are subscribed to the Google 
> Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to smt-lib+unsubscribe at googlegroups.com 
> <mailto:smt-lib+unsubscribe at googlegroups.com>.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/smt-lib/002f01d6fbee%242154eb90%2463fec2b0%24%40ist.utl.pt 
> <https://groups.google.com/d/msgid/smt-lib/002f01d6fbee%242154eb90%2463fec2b0%24%40ist.utl.pt?utm_medium=email&utm_source=footer>.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 495 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20210205/2fdb42b9/attachment-0001.sig>