[SMT-LIB] QF_BV and division by zero

[Florian Schanda]

On Wednesday 14 Oct 2015 22:08:01 Clark Barrett wrote:
> 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:

Hm, not sure I am totally convinced, I've always been more happy with the 
current "uninterpreted function" behaviour. But I do certainly see *why* 
solver writers might prefer the fixed interpretation.

This issue is very similar to the fp.min and fp.max issue to me; could we not 
use a similar solution (i.e. make it configurable)?

	Florian