[SMT-LIB] QF_BV and division by zero

[Tjark Weber]

On Wed, 2015-10-14 at 22:08 -0700, Clark Barrett wrote:
> So, we are proposing to change the semantics of bit-vector division so
> that division by zero produces a vector of all 1's.

I still believe that this is not a very good idea. Already today, one
of the most common problems in the application of formal methods is
that users do not model their systems correctly.

The proposed change makes life slightly easier for solver developers,
but it shifts the burden to the users of bit-vector logics. Users will
need to be aware that it is no longer sound to simply use 'bvdiv' to
model bit-vector division, *unless* the system that they are modeling
happens to guarantee that the result of division by 0 is all 1's.

I am guessing it won't be very long until someone uses 'bvdiv' in an
unsound manner because they were not aware of this subtlety.

However, it appears that you've already weighed this argument. I do
welcome that this semantic issue is being resolved at last. Any clear
resolution is an improvement over the current situation, and hopefully
will allow us to include benchmarks that use bit-vector division in the
SMT Competition again next year.

Best,
Tjark