[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

Hi,

I just saw the call for benchmarks.

I'd like to state I intend to contribute a set of benchmarks

* Some QF_FPBV benchmarks
* A new category that I suggested some time ago that mixes the
theories of quantifier free floating point and arrays of bitvectors. I
suggest the name QF_FPABV

I should have preliminary version of these benchmarks available in the
next few days.

A few questions:

* Do I need to curate these benchmarks in some way. If so what
criteria should I use? E.g. Should I pick the longest running? I have
quite a few benchmarks (~ 8000) so having that many might not be
desirable.
* Some benchmarks may use Z3's non-standard fp.to_ieee_bv function. Is
that a problem?
* The QF_FPBV and QF_FPABV benchmarks will be very similar because
they come from the same source (the QF_FPBV benchmarks are QF_FPABV
benchmarks where we have been able to remove arrays using knowledge of
our problem domain). Is this a problem?
* Many benchmarks do not have a known answer. Is that a problem?
* Are there any requirements about what needs to be in the pre-amble
of the smt2 file? (.e.g Does the logic need to be stated?).

Thanks,
Dan.