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

[Dejan Jovanović]

Ok, I'll take it that handling division as in the standard is to be
expected then.

It would be nice to have a discussion about this in the wider context of
SMTLIB and undefined behavior. I see it less about the current solvers
giving correct answers, and more about consistency and reducing the barrier
to entry. As with bit-vectors it's not clear that this semantics for
division are ideal. Also, we'd like to encourage people to do develop new
solvers and participate, and addition of UF can be quite a burden if the
solver doesn't already support it.

Does anyone else have an opinion on this?

Cheers, Dejan

On Sun, May 15, 2016 at 10:07 AM Tjark Weber <tjark.weber at it.uu.se> wrote:

> 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
>
>