[SMT-LIB] QF_BV and division by zero

[Alberto Griggio]

Hi Clark,

> Hi all,
>
> We've had many discussions about the semantics of division by zero in the
> bit-vector theory.  After the most recent discussion at the SMT workshop,
> it became clear that the arguments for fixing an interpretation seem to
> outweigh the arguments for the current semantics.  So, we are proposing to
> change the semantics of bit-vector division so that division by zero
> produces a vector of all 1's.  The rationale is:

[...]

> A new version of bit-vectors with this proposed change will be available
> for comment soon.  In the meantime, feedback is welcome.

A big +1 from me (as you might know :-)

Alberto