Method add_no_usoverflow

smt/expr.cpp:880–885

}

expr expr::add_no_usoverflow(const expr &rhs) const {
  if (min_leading_zeros() >= 1 && rhs.min_leading_zeros() >= 1)
    return true;

  return (zext(1) + rhs.sext(1)).sign() == 0;
}

expr expr::sub_no_soverflow(const expr &rhs) const {
  if (min_leading_zeros() >= 1 && rhs.min_leading_zeros() >= 1)