Support for overflow and underflow operators over bv

[agurfinkel]

Both Z3 and Boolector provide API to detect whether arithmetic over bit-vectors overflows/underflows. This seems to be missing from Yices. Is there some good way to get similar functionality. I assume that Z3 implementation is based on the following report:

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf

[dddejan]

Can you point to the API for reference.

[agurfinkel]

In Z3, the relevant API start here: https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h#L2996

In Boolector, look for operators that end with o. Like this one: https://github.com/Boolector/boolector/blob/master/src/boolector.h#L1154