Method srem

smt/expr.cpp:776–787

}

expr expr::srem(const expr &rhs) const {
  if (eq(rhs) || isZero() || (isSMin() && rhs.isAllOnes()))
    return mkUInt(0, sort());

  if (rhs.isZero())
    return rhs;

  if (isNegative().isFalse() && rhs.isNegative().isFalse())
    return urem(rhs);

  return binop_fold(rhs, Z3_mk_bvsrem);
}

expr expr::urem(const expr &rhs) const {
  C();