mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Fixed MPF fp.rem(0,0,0). Relates to #872.
This commit is contained in:
parent
79ab8a5a5a
commit
4ff938f2c1
|
@ -797,9 +797,9 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
|
|||
set(o, z);
|
||||
}
|
||||
else if (is_zero(x) || is_zero(y)) {
|
||||
bool xy_sgn = is_neg(x) ^ is_neg(y);
|
||||
if (is_zero(z) && xy_sgn ^ is_neg(z))
|
||||
mk_zero(x.ebits, x.sbits, rm != MPF_ROUND_TOWARD_NEGATIVE, o);
|
||||
bool xy_sgn = sgn(x) ^ sgn(y);
|
||||
if (is_zero(z) && (xy_sgn ^ sgn(z)))
|
||||
mk_zero(x.ebits, x.sbits, rm == MPF_ROUND_TOWARD_NEGATIVE, o);
|
||||
else
|
||||
set(o, z);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue