Method mul_no_soverflow

smt/expr.cpp:897–900

}

expr expr::mul_no_soverflow(const expr &rhs) const {
  auto bw = bits();
  return sext(bw) * rhs.sext(bw) == (*this * rhs).sext(bw);
}

expr expr::mul_no_uoverflow(const expr &rhs) const {
  auto bw = bits();