[SMT-LIB] QF_BV and division by zero

[Clark Barrett]

Hi all,

Changes have been made to the theory of bitvectors.  Specifically, bvudiv
now returns a vector of all 1's if the second operand is 0 and bvurem
returns its first operand if the second operand is 0 (note that this also
affects the operators defined in terms of these two).  This is detailed in
the online descriptions of the theory FixedSizeBitVectors and the logic
QF_BV, both available on the smtlib.org website.  Before the benchmark
release on June 1, all benchmarks will be checked and their statuses
updated if affected by these changes.

-Clark