[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

Hi,

On 23 April 2017 at 20:29, Delcypher <delcypher at gmail.com> wrote:
> Hi,
>
> On 21 April 2017 at 16:06, Christoph Wintersteiger
> <cwinter at microsoft.com> wrote:
>> Hi Dan,
>>
>> Space is free, 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.
>>
>> In other parts of the library it turned out that we had a bunch of duplicates with different file names (e.g. QF_BV/sage2 if I remember correctly). If there's an easy way for you to filter those, that would be nice.
>
> Finally! I have the first version of the benchmarks for consideration.
> I'm sorry that this took so long. I had a lot of false starts.
>
> Good call on asking me to remove duplicates (I used the fdupes tool
> for this). This found a bug in my tool because it is supposed to cache
> query results so for a single run of my tool there should have been no
> duplicates but it turns out were some!
>
> They are available at
> https://www.doc.ic.ac.uk/~dsl11/assets/qf_fpabv_qf_fpbv_liew_v0.tar.xz
>
> These have been annotated with
>
> * The logic
> * Satisfiability if known. This was determined by running Z3 and
> Mathsat5 on the benchmarks before doing any annotation. I suspect the
> `QF_FPABV` logic annotation might confuse the solvers but I've not
> tried. I allowed at most 30 minutes per query
> * A note regarding a corresponding equisatisfiable query if it exists
>
> A few statistics:
>
> Number of benchmarks by logic:
> QF_FPABV: 18033 benchmarks
> QF_FPBV: 17156 benchmarks
>
> Number of benchmarks by satisfiability:
> 28099 sat benchmarks
> 7070 unsat benchmarks
> 20 unknown benchmarks
>
> Please take a look and let me know if you find any problems. If you or
> others wish to remove benchmarks please discuss this with me first.
> Doing so without care will breaks the comments in the benchmarks
> noting about corresponding equisatisfiable benchmarks in the other
> logic.

I don't know if you've had a chance to look yet but I noticed I didn't
attribute all the authors of the benchmarks that I should have.
I've produced a revised version which fixes this which is available at
the link below.

https://www.doc.ic.ac.uk/~dsl11/assets/qf_fpabv_qf_fpbv_liew_v1.tar.xz

I'm keen to get feedback on this so please take a look. Again if you'd
like me to trim down the number of benchmarks I'm happy to do this but
I need to the okay from Christoph because he will become the owner of
these benchmarks.

Thanks,
Dan.