[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

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.

Thanks,
Dan.