Method mul_no_uoverflow

smt/expr.cpp:902–905

}

expr expr::mul_no_uoverflow(const expr &rhs) const {
  auto bw = bits();
  return (zext(bw) * rhs.zext(bw)).extract(2*bw - 1, bw) == 0;
}

expr expr::sdiv_exact(const expr &rhs) const {
  return sdiv(rhs) * rhs == *this;