[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Clark Barrett]

I second Tjark's comment.  The SMT-LIB policy is that a status attribute is
set only when the status is known.  There should not be any element of
speculation - if there is, the status should remain unknown.

I also agree that this is a separate issue from whether unknown benchmarks
can or should be included in the competition.  I think that having an
"unknown track" might be a very useful and interesting extension to the
competition.

I'd also just like to note that the SMT-LIB maintainers and SMT-COMP
committee members are working on establishing better documentation and
protocols around determining status.  We will announce these once the
conversation has converged.

-Clark

On Mon, Apr 10, 2017 at 4:40 AM, Tjark Weber <tjark.weber at it.uu.se> wrote:

> Dan,
>
> On Fri, 2017-04-07 at 11:39 +0100, Delcypher wrote:
> > Is it okay to put these "unknown" benchmarks as "unsat"?
>
> Please do not do this! Status information in SMT-LIB benchmarks ought
> to be correct.
>
> Whether benchmarks with unknown status should be included in the
> competition is a separate question that we are currently debating. But
> simply setting an arbitrary (possibly incorrect) status would lead to
> problems when these benchmarks are used in the competition, and would
> most likely result in their retroactive disqualification.
>
> Best,
> Tjark
>
>
>