This PR adds SMT-LIB operators to detect overflow
`BitVec.(uadd_overflow, sadd_overflow)`, according to the definitions
[here](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorems proving equivalence of such definitions with the
`BitVec` library functions (`uaddOverflow_eq`, `saddOverflow_eq`).
Support theorems for these proofs are `BitVec.toNat_mod_cancel_of_lt,
BitVec.toInt_lt, BitVec.le_toInt, Int.bmod_neg_iff`. The PR also
includes a set of tests.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
0ed493e748