feat: add SMT-LIB overflow on addition for bitvectors (`uadd_overflow`,`sadd_overflow`, `uadd_overflow_eq`,`sadd_overflow_eq`) and support theorems #14467