[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Clark Barrett]

Hi Dan,

Let me try to answer your 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.

This is really up to you, but generally my hope would be a set of
benchmarks that does a good job of representing all the diversity of the
entire set of benchmarks.  If this means you can prune some, great.  But
you should be sure to include representatives from different difficulty
levels, different sizes, different statuses, different applications etc.

* Some benchmarks may use Z3's non-standard fp.to_ieee_bv function. Is
that a problem?

This is definitely a problem for including them in SMT-LIB.  You either
need to make a case for extending the standard, find a way to encode the
benchmarks with this construct in a different way, or we will have to
exclude the benchmarks with this operator.

* 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?

No - in fact it's often interesting to include the same benchmarks using
different encodings.  Each set of benchmarks should explain that they come
from the same source though, so people understand the relationship.

* Many benchmarks do not have a known answer. Is that a problem?

We encourage you to set the status if it is known, but you can also submit
benchmarks with unknown status.

* 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?).

Yes.  We recently set up a repository for benchmark submissions which
includes instructions about the pre-amble.  Please refer to those
instructions which are here:
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending

-Clark