[SMT-LIB] QF_BV and division by zero

[Tjark Weber]

Clark,

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.

What is the status of this proposal?

The theory definition at http://smtlib.cs.uiowa.edu/theories-FixedSizeB
itVectors.shtml, last updated 2016-04-20, "do[es] not specify the
meaning of (bvudiv s t) or (bvurem s t) in case bv2nat([[t]]) is 0."

Best,
Tjark