[SMT-COMP] QF_FP, min and zeros

François Bobot francois.bobot at cea.fr
Fri Apr 21 06:04:34 EDT 2017

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?



More information about the SMT-COMP mailing list