[SMT-LIB] QF_BV and division by zero

[Clark Barrett]

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:

1. Bit-vectors are used to represent machine/circuit calculations.  A
circuit computes a value if zero is fed as an input.  The value it computes
is all 1's.

2. The current semantics were designed to help users find bugs, but they
still allow certain kinds of bugs to go masked.  For instance, the
semantics of first-order logic enforce that dividing the same number by 0
in two different places yields the same result.

3. Users have the freedom to encode bit-vector division however they like,
including using a unique uninterpreted function for every occurrence of
division.

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

-Clark