Call For Benchmarks

[Jochen Hoenicke]

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.

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

[Andrew Jones]

Hi,

I am interested in submitting some *incremental* instances to QF_FP
(55 instances), QF_BVFP (46 instances) and QF_ABVFP (1550 instances).
These instances will be generated using Z3's logging capability.

I started this work last year (with the help of Mathias Preiner), but
it somewhat stagnated (I am not sure why). I will revisit this to
clean these benchmarks-up and get them submitted ASAP.

Cheers,

Andrew

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CANYHNmKXUVw4hZx3tho-cif-HOm5qf%3DGjsBfrNM3VwHCbPB8Nw%40mail.gmail.com.

[Nuno Lopes]

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

[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-...@cs.nyu.edu; smt...@googlegroups.com
> *Cc:* Antti Hyvärinen <antti.h...@gmail.com>; Haniel Barbosa
> <hanielb...@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+u...@googlegroups.com

> <mailto:smt-lib+u...@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>.

[Nuno Lopes]

Ok, sounds good! I'll filter out the benchmarks with lambdas and send you a few hundred files.
Nuno

To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/3f63b29e-9d61-32a3-20e8-3e0abfddf89e%40gmail.com.

[Aina Niemetz]

Nuno,

can you maybe also include some of the ones that Z3 solves under 1s?
Only a few is already enough, just as a sanity check -- if other solvers
are slow on those, they are certainly interesting.

Thanks a lot!
Aina