[SMT-COMP] QF_FP, min and zeros

[Tjark Weber]

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