Overflow checking for symbolic add/sub

[ghost]

This adds overflow checks for abstract addition and subtraction. intrinsic_with_overflow can now store an abstract PrimVal for the overflow bool. This allows the compiler-inserted Asserts to be evaluated meaningfully for Add and Sub with at least one abstract operand.

Some of the function signatures in operator.rs have been changed: instead of returning a bool to indicate overflow, a PrimVal is used. This allows us to return abstract values when needed.

I ran into some trouble with tests failing because intrinsic_overflowing had to return a bool. If the overflow PrimVal is abstract, conversion to bool is unimplemented!(). The workaround returns to the old behavior of just returning false (no overflow) for all abstract ops. From a quick search of the codebase, it seems like none of the users of the function actually use the returned overflow bool. It might be a better solution to just remove the overflow bool from the return value.

A few other tests failed because Seer stops at the first panic, which ended up being an overflow. I replaced the adds with wrapping_add, which prevents the insertion of overflow checks.

[dwrensha]

Thanks! I expect I'll have time to take a look this weekend.

[dwrensha]

Looks good to me!