| 745 | } |
| 746 | |
| 747 | expr expr::sdiv(const expr &rhs) const { |
| 748 | if (eq(rhs)) |
| 749 | return mkUInt(1, sort()); |
| 750 | |
| 751 | if (rhs.isZero()) |
| 752 | return rhs; |
| 753 | |
| 754 | if (isZero() || rhs.isOne()) |
| 755 | return *this; |
| 756 | |
| 757 | if (isSMin() && rhs.isAllOnes()) |
| 758 | return mkUInt(0, sort()); |
| 759 | |
| 760 | return binop_fold(rhs, Z3_mk_bvsdiv); |
| 761 | } |
| 762 | |
| 763 | expr expr::udiv(const expr &rhs) const { |
| 764 | if (eq(rhs)) |