[SMT-COMP] QF_FP, min and zeros

[François Bobot]

Le 20/04/2017 à 19:56, Martin Nyx Brain a écrit :
> On Thu, 2017-04-20 at 17:45 +0200, François Bobot wrote:
>> As a side note, Wintersteiger is great and invaluable as a set of unit tests, but it should not be
>> used for the competition. But perhaps it will not since it is crafted.
>
> IMHO It rather depends on what you want the competition to assess.
>

In the completely different field of robot competition, before the main challenges a first stage of 
selection is done with simple tests: moving from one point to another, shooting a ball inside the 
goal (in the case of soccer robot).

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?

Cheers,

-- 
François