Method fdiv

smt/expr.cpp:1244–1247

}

expr expr::fdiv(const expr &rhs, const expr &rm) const {
  C(rhs, rm);
  return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs);
}

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