Consider divide by zero

[pirapira]

A division instruction should produce two behaviors, one for divide by zero and the other for divide by non-zero. (When the divisor is known to be non-zero, only one behavior is fine.)

Instructions involving division return zero when the divisor is zero. This should be taken into account for *DIV and *MOD instructions.

[pirapira]

Or, we can cut corners by saying "a / 0 = 0 for any a" (like in ssreflect).