mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-05-08 21:30:01 -07:00
commit 4080cddb68
2 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -959,14 +959,14 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
c3 = y_is_inf;
v3 = x;
// (x is 0) -> x
c4 = x_is_zero;
v4 = pzero;
// (y is 0) -> NaN.
c5 = y_is_zero;
v5 = nan;
c4 = y_is_zero;
v4 = nan;
// (x is 0) -> x
c5 = x_is_zero;
v5 = pzero;
// else the actual remainder.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());

4
src/util/mpf.cpp
View file

@ -1099,10 +1099,10 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
mk_nan(x.ebits, x.sbits, o);
else if (is_inf(y))
set(o, x);
else if (is_zero(x))
set(o, x);
else if (is_zero(y))
mk_nan(x.ebits, x.sbits, o);
else if (is_zero(x))
set(o, x);
else {
o.ebits = x.ebits;
o.sbits = x.sbits;