fix: Unsound interval rules for *, div, mod, / and **

[fabiomadge]

Five of the domain's arithmetic rules inferred bounds that need not hold. * with two negative lower
bounds claimed the product is at most their product. div, mod and / accepted a divisor whose lower
bound is zero, where division is underspecified. ** claimed a lower bound of 1 for a nonzero exponent
and took its upper bound from the exponent.

procedure P(x: int, y: int) returns (p: int)
{
  assume -3 <= x;
  assume -3 <= y;
  p := 0;
  while (p == 0) { p := x * y; }
  assert p <= 9;
}

-infer:j → 1 verified, 0 errors, though x * y is unbounded above. The loop is there only because
inferred facts reach the prover at loop heads.

Fix. * keeps the nonnegative case alone, since a negative operand needs all four corner products and
so an upper bound on both. The three divisions require 1 <= lo1, which also makes div and / identical
and lets them share a case — the merged rule is correct under both the half-open reading ints get and the
closed one reals get. ** loses its rule.

Testing. Three files covering all five rules. ** cannot be caught by a false assertion, because it is
emitted as real_pow, which the background predicates declare only under a non-monomorphic encoding, so
any verification condition mentioning it dies in the solver (#1166 fixes that). PowerBounds.bpl checks
the inferred invariant directly under -noVerify, where master infers the false 1e0 <= p && p <= 2e0
for x ** y with x >= 0 and 1e0 <= y <= 2e0.

One of six.