Handle division by zero for non-negative types

[Philipp15b]

When a user writes a/b and the result is a non-negative type, then we currently do not restrict the result to be non-negative. This is relevant when b = 0 holds, in which case the SMT solver can assign any value to a/0, including negative numbers. If used as expectations, this can break all kinds of assumptions, including error reporting by slicing. I have observed a counterexample where all assertions were sliced because of this (which should not be possible).

[Philipp15b]

Here's an example where error reporting currently reports no asserts as failing because the division by zero is causing problems.

coproc algorithm_r_wrong(n: UInt, x: UInt) -> (c: UInt)
    pre !?(n > 0 && n >= x && x >= 1)
    pre 1/n
    post [c == x]
{
    c = 0
    var i: UInt = 1
    @invariant((1/(n-(i+1))) * [i <= x && x <= n] + [x == c])
    while i <= n {
        var prob_choice: Bool = flip(1/i)
        if prob_choice {
            c = i
        } else {}
        i = i + 1
    }
}

With cex:

Counter-example to verification found!

extra definitions:
    /0: [[1.0, 1.0] -> 1.0, else -> (- 2.0)]

the pre-quantity evaluated to:
    ∞

in the sliced program, the pre-quantity evaluated to:
    ∞
    (slicing removed 3/3 assertions)
in the cex, input variable n is 1
in the cex, input variable x is 1
in the cex, bound variable i is 0
in the cex, bound variable c is 1