fix: Abstract interpretation proves false assertions about arithmetic - #1159

Five of the interval 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 that may be zero,
which leaves the result unspecified. ** claimed a lower bound of 1 for an exponent of at least 1 and took its
upper bound from the exponent, though 0.5 ** 1.0 is 0.5 and 3.0 ** 2.0 is 9.0.

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

-infer:j → 1 verified, 0 errors, though x = y = 4 gives 16. The loop is there only because inferred facts
reach the prover at loop heads. Dafny turns this inference on by default and maps * on reals to Boogie's *,
so there the same pattern over reals proves false without any flags.

Fix. * keeps only its nonnegative case, and the divisions require a divisor of at least 1. That makes the
div and / rules identical, so they now share a case, whose bounds /checkInfer proves for int and real
operands alike. ** loses its rule.

Testing. ArithmeticBounds.bpl asserts each false bound; master verifies every one. ** is emitted as
real_pow, which a monomorphic program leaves undeclared until #1166, so PowerBounds.bpl checks the inferred
invariant under -noVerify instead, where master infers 1e0 <= p && p <= 2e0. It should land before #1166:
with that alone, master proves such false ** assertions. Linear5.bpl.expect had recorded the false x < 2
after -1 <= x and x := x*x. Dafny's 130 test files that use reals and reach the verifier give the same
results with this change.

One of six.