[SMT-LIB] QF_BV and division by zero

[Martin Nyx Brain]

On Fri, 2017-03-31 at 23:07 -0700, Clark Barrett wrote:
> Hi everyone,
> 
> Yes, this should have been finalized last year and it's my fault it wasn't
> - I'm very sorry :(
> We have discussed this far too many times, but let's fix it finally.

(Can I just clarify this is the discussion about bit-vector divide /
remainder by zero and not any of the other partially interpreted
functions?)

<snip>
> The main reason to fix the interpretation is to make solver development for
> QF_BV more clear and straightforward.
> 
> Trevor, you are arguing for a value of 0, but do you disagree that a vector
> of 1's is the most natural result from a circuit?  What do others think
> about his argument for 0?

<unhelpful and can be ignored>
That rather depends on what kind of circuit you use.  For example, you
could reduce x = a/b  to  b * x + r == a  &&  0 <= r < x  which we've
tried with some performance benefit.
</unhelpful and can be ignored>

Cheers,
 - Martin