[SMT-LIB] QF_BV and division by zero

[Tjark Weber]

Viktor,

On Thu, 2015-10-15 at 12:27 +0000, Viktor Kuncak wrote:

> Uninterpreted semantics gives only an illusion that one can use simple
> modeling. Many formal methods applications will have non-deterministic
> behavior for errors, so deterministic uninterpreted functions are
> making the problem more subtle instead of solving it. [...]

I agree that the current semantics is still too strong for many
applications. Clark made the same point, cf. item 2. of his email.

In my view, this is a good argument for an even weaker semantics.
Unfortunately, however, a fully non-deterministic semantics cannot be
achieved within the current semantic foundations of SMT-LIB.

> So, if the proposed change means that now more people will realize
> that they need to explicitly model behaviors where the source system
> gives an error, that, in my view, will be a good thing.

I agree, but I don't quite see why the proposed change would mean that.

Users who will benefit are those who read the specification of 'bvdiv'
and realize that "all 1s" is not a correct semantics for their
application, but who failed to realize that "some unspecified
bit-vector value" was not a correct semantics either.

My concern lies with users who will simply (naively) use 'bvdiv' to
model bit-vector division, and not think about this twice unless they
have to (for instance, because the SMT solver cannot prove some of
their verification conditions). For this group, a stronger semantics
means that the SMT solver is less likely to point out their mistake.

I suppose it is anyone's guess which group of users is larger.

Best,
Tjark