[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks
barrett at cs.stanford.edu
Tue Apr 11 18:05:47 EDT 2017
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
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.
On Mon, Apr 10, 2017 at 4:40 AM, Tjark Weber <tjark.weber at it.uu.se> wrote:
> 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.
More information about the SMT-COMP