Use Spans in cases where we can't infer them exactly (#9034)

`x < 10` can be turned into `Span{0,10}` exactly, but we can actually infer
something from `x < y` even though `y` is unknown: x cannot be MAX_INT.
That is, we can prove the Span must be contained in `Span{0, MAX_INT-1}`
even if we can't provide an exact span.

To use this, move the `getSpan()` users out of the code that handles
constant constraints and into where non-constant ones are handled. Then
just use `getProvenSpan` instead of `getSpan` where possible.

This is important for certain loops (later PRs will depend on this).