[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

Hi,

On 22 April 2017 at 18:29, Cesare Tinelli <cesare-tinelli at uiowa.edu> wrote:
> Hi all,
>
> On 21 Apr 2017, at 10:06, Christoph Wintersteiger wrote:
>
>> Hi Dan,
>>
>> Space is free,
>>
> That is, payed for by someone else :)  (The SMT-LIB coordinators, StarExec,
> etc.)
>
>> submit them all! If it turns out there are too many of them, we can let
>> others (e.g. the competition organizers) do the sub-sampling themselves and
>> by their own criteria.
>>
> Depending on how big the benchmark submission is, it may actually be
> necessary to create a selection for SMT-LIB, as opposed to just SMT-COMP.
>
> We have moved the master copy of the SMT-LIB benchmarks to a GitLab server
> (at Iowa, with a mirror at INRIA, to be announced officially soon). While
> this is ultimately going to be more convenient for everybody, git does not
> work very well with very large repositories or very large files. So,
> although disk space is not necessarily a concern, the size of a repository
> is.
>
> Perhaps Dan can still send all of his benchmarks to Christoph, and then we
> can work on a sample internally for SMT-LIB inclusion.

Please don't do this internally. If you need to do this please discuss
it with me. The benchmarks are not entirely independent of each other
(they contain comments noting an equisatisfiable query in the other
logic if it exists) so removing benchmarks without care will break
these comments. I have also run every single benchmark through Z3 and
Mathsat5 so I can very easily filter out queries that I consider to be
interesting (those that take > 10 seconds to solve). When I looked at
the distribution of solver execution times over my benchmarks the
majority of benchmarks are solved very quickly so I can use that to
sample the set of benchmarks by giving the slow running benchmarks
more priority.

Thanks,
Dan.