| 803 | } |
| 804 | |
| 805 | expr expr::sadd_sat(const expr &rhs) const { |
| 806 | expr add_ext = sext(1) + rhs.sext(1); |
| 807 | auto bw = bits(); |
| 808 | auto min = IntSMin(bw); |
| 809 | auto max = IntSMax(bw); |
| 810 | return mkIf(add_ext.sle(min.sext(1)), |
| 811 | min, |
| 812 | mkIf(add_ext.sge(max.sext(1)), |
| 813 | max, |
| 814 | *this + rhs)); |
| 815 | } |
| 816 | |
| 817 | expr expr::uadd_sat(const expr &rhs) const { |
| 818 | return mkIf(add_no_uoverflow(rhs), |