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

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