[SMT-LIB] QF_BV and division by zero

[Trevor Hansen]

It'd be great to have QF_BV division and remainder by zero resolved in time for this year's SMTCOMP.
The relevant discussion from 2015 is in the thread here:http://www.cs.nyu.edu/pipermail/smt-lib/2015/000966.html

Personally, I'd prefer division and remainder by zero to evaluate to zero. Because then the semantics of bvsdiv, bvsrem and bvsmod by zero are simpler. 
bvsdiv, bvsrem, and bvsmod are defined here: http://smtlib.cs.uiowa.edu/logics-all.shtml

For example, bvsrem is:  (bvsrem s t) abbreviates
      (let ((?msb_s ((_ extract |m-1| |m-1|) s))
            (?msb_t ((_ extract |m-1| |m-1|) t)))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
             (bvurem s t)
        (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
             (bvneg (bvurem (bvneg s) t))
        (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
             (bvurem s (bvneg t)))
             (bvneg (bvurem (bvneg s) (bvneg t))))))
So if 's' is negative, whatever bvurem-by-zero evaluates to needs to be negated.  This means that if unsigned division/remainder evaluate to all ones, then (bvsdiv s 0),  (bvsrem s 0), (bvsmod s 0) all evaluate to all-ones if 's' is positive, and 1 if 's' is negative. This seems like an unnecessary complication.
However, if (bvudiv s 0) and (bvurem s 0 ) evaluate to zero, then (bvsdiv s 0), (bvsrem s 0), (bvsmod s 0) also evaluate to zero. Levent Erkok commented that this how many theorem provers implement the semantics. So it seems simplest to me.

Unless anyone has objections, I'll try to get a consensus from other QF_BV solver developers that division/remainder by zero evaluates to zero is the best way forward?
Thanks,
Trev.