mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge pull request #236 from wintersteiger/i68

Browse source 
Fixes for issue #68
This commit is contained in:
Christoph M. Wintersteiger 2015-10-07 20:56:35 +01:00
commit b60f30c802
13 changed files with 283 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/util/mpf.cpp
View file

@ -1250,12 +1250,13 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) {
UNREACHABLE(); // max(+0, -0) and max(-0, +0) are unspecified.
}
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (gt(x, y))
set(o, x);
else
@ -1265,12 +1266,13 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x))
set(o, y);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y))
mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (is_nan(y))
set(o, x);
else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) {
UNREACHABLE(); // min(+0, -0) and min(-0, +0) are unspecified.
}
else if (is_zero(x) && is_zero(y))
set(o, y);
else if (lt(x, y))
set(o, x);
else