[SMT-COMP] QF_FP, min and zeros

[Christoph Wintersteiger]

Hi all,

I think that's a good idea and this is exactly what those benchmarks have been designed to do. I agree that we can't make it mandatory for all participants to run regression tests for all logics/theories beforehand, but in the case of FP we can definitely send an extra email to all participants making them aware of the latest version of these test cases, just to make sure they have a "reference" set to look at when they are unsure. 

Cheers,
Christoph

-----Original Message-----
From: smt-comp-bounces at cs.nyu.edu [mailto:smt-comp-bounces at cs.nyu.edu] On Behalf Of Tjark Weber
Sent: 21 April 2017 12:16
To: François Bobot <francois.bobot at cea.fr>
Cc: smt-comp at cs.nyu.edu
Subject: Re: [SMT-COMP] QF_FP, min and zeros

François,

On Fri, 2017-04-21 at 12:04 +0200, François Bobot wrote:
> A similar stage can be done in our case, running all the 
> Wintersteiger's unit test with a timeout of 1s and eliminating the 
> provers that give a wrong result. But these benchmarks would not be 
> used for the provers comparison because the real examples are lost 
> among the unit tests.
> 
> What do you think of that?

Note that the competition comprises 3 tracks and over 40 divisions (logics). To keep this manageable, we shouldn't overcomplicate its design.

At this point, I am inclined to believe that unit tests (i) can serve an important purpose in identifying incorrect solver implementations, and (ii) do not necessarily cause "real" examples to be "lost": if solving unit tests is easy, state-of-the-art solvers will only differ in how many of the real examples they can solve, so the (relative) ranking will depend on those.

Best,
Tjark


_______________________________________________
SMT-COMP mailing list
SMT-COMP at cs.nyu.edu
https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fcs.nyu.edu%2Fmailman%2Flistinfo%2Fsmt-comp&data=02%7C01%7Ccwinter%40microsoft.com%7Cebf46c6061e740036d6408d488aa2e1a%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636283711878986812&sdata=X4PCUGYopwhtwDoPq7Mc9OjWRte%2BapWdlwXNFN0Q0Lc%3D&reserved=0