| 761 | } |
| 762 | |
| 763 | expr expr::udiv(const expr &rhs) const { |
| 764 | if (eq(rhs)) |
| 765 | return mkUInt(1, sort()); |
| 766 | |
| 767 | if (rhs.isZero()) |
| 768 | return rhs; |
| 769 | |
| 770 | if (isZero() || rhs.isOne()) |
| 771 | return *this; |
| 772 | |
| 773 | return binop_fold(rhs, Z3_mk_bvudiv); |
| 774 | } |
| 775 | |
| 776 | expr expr::srem(const expr &rhs) const { |
| 777 | if (eq(rhs) || isZero() || (isSMin() && rhs.isAllOnes())) |
no test coverage detected