[SMT-COMP] SMT-COMP 2016: Incorrect Answers (Unknown Track)

[Tjark Weber]

Dejan,

On Fri, 2016-07-15 at 18:09 +0000, Dejan Jovanović wrote:


> Bruno examined the data from starexec and you can see it summarized
> here:
> https://docs.google.com/spreadsheets/d/1V0Wu5RE1pHDa1inOviJ5i7xte1yo8h6eFElCKjHKfpY/edit?usp=sharing

> The situation is not nearly as bad as in your table.

Thank you for this more detailed analysis!

> More interestingly, raSAT seems to be printing unsat on timeouts
> (which is a bit worrying considering that this didn't show up in the
> main competition).

It actually showed up also in the main track: see
http://smtcomp.sourceforge.net/2016/results-QF_NIA.shtml

The raSAT developer is aware of the issue.

Note that there was a rule change this year to take solver output into
account also when the solver times out. In previous years, these
incorrect answers would have been disregarded.

Best,
Tjark