| 736 | } |
| 737 | |
| 738 | expr expr::operator*(const expr &rhs) const { |
| 739 | unsigned power; |
| 740 | if (rhs.isConst() && is_power2(rhs, power)) |
| 741 | return *this << mkUInt(power, sort()); |
| 742 | if (isConst() && is_power2(*this, power)) |
| 743 | return rhs << mkUInt(power, sort()); |
| 744 | return binopc(Z3_mk_bvmul, operator*, Z3_OP_BMUL, isOne, isZero); |
| 745 | } |
| 746 | |
| 747 | expr expr::sdiv(const expr &rhs) const { |
| 748 | if (eq(rhs)) |