[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Giles Reger]

Hi,

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

Is it okay to put these "unknown" benchmarks as "unsat"? I really want
them included in the competition so solver
writers are encouraged to try improve performance on these difficult
benchmarks. If putting them as "unknown"
means they won't be used in the competition I'd rather just label them
as "unsat" and note in the description that
this has not been confirmed.

I understand this attitude. This is one of the reasons the Call for Comments asked people to comment on benchmarks with unknown status in the competition. I repeat the question here.

- Benchmarks with unknown status: Previous SMT-COMPs have only used
 benchmarks whose status (sat/unsat) was known. One might argue that
 this favors imitation of existing solvers over innovation. Should
 benchmarks with unknown status be used in the competition? If so,
 how should answers for such benchmarks be scored? Can scoring for
 one solver remain independent of the answers given by other solvers,
 or should disagreements between solvers lead to negative scores for
 a solver?

I believe from your comments that you think that benchmarks with unknown status should be used in the competition, do you have any other comments related to this question? We are keen to have a dialogue on this, potentially controversial, topic.

Cheers, Giles