[SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[Tjark Weber]

Dejan,

On Sun, 2016-05-15 at 15:56 +0000, Dejan Jovanović wrote:
> The issue is basically the same as in bit-vectors, i.e. to properly
> support it one has to involve extra reasoning with uninterpreted
> functions. Since the issue is the same as in bit-vectors, my thinking
> is that it would be best to use the same policy for inclusion in the
> competition.

I understand the similarity with bit-vector division. However,
considering that these benchmarks have been used in past competitions
without apparent problems, I would be reluctant to exclude benchmarks
that use integer/real number division just on similarity grounds, and
without a wider discussion. (Also, it is not clear to me that we could
easily distinguish between guarded and unguarded use.)

Are there solvers that handle unguarded (integer/real number) division
incorrectly, or SMT-LIB benchmarks that have been assigned an incorrect
status?

> There was lots of discussion about it so I don't remember anymore,
> are bit-vector benchmarks with unguarded division included in the
> competition?

Not in 2016.

Best,
Tjark