mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +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 73eb7cbf5c
commit 53b479e1c3
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

@ -1161,10 +1161,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;