mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Bugfix for fp.rem(0, 0).

Browse source 
Fixes #70.
This commit is contained in:
Christoph M. Wintersteiger 2015-05-06 12:24:18 +01:00
parent 901d8a9f5b
commit 31e78cd178
2 changed files with 8 additions and 8 deletions
Show stats 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; c3 = y_is_inf;
v3 = x; v3 = x;
// (x is 0) -> x
c4 = x_is_zero;
v4 = pzero;
// (y is 0) -> NaN. // (y is 0) -> NaN.
c5 = y_is_zero; c4 = y_is_zero;
v5 = nan; v4 = nan;
// (x is 0) -> x
c5 = x_is_zero;
v5 = pzero;
// else the actual remainder. // else the actual remainder.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(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); mk_nan(x.ebits, x.sbits, o);
else if (is_inf(y)) else if (is_inf(y))
set(o, x); set(o, x);
else if (is_zero(x))
set(o, x);
else if (is_zero(y)) else if (is_zero(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else if (is_zero(x))
set(o, x);
else { else {
o.ebits = x.ebits; o.ebits = x.ebits;
o.sbits = x.sbits; o.sbits = x.sbits;