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 hwf_manager::rem

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-24 15:11:24 +01:00
parent 3131f29816
commit 952e3afb90
1 changed files with 2 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/util/hwf.cpp
View file

@ -383,17 +383,10 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
} }
void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) { void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {
// The built-in fmod() works, except for the special numbers. o.value = remainder(x.value, y.value);
if (is_inf(x) && is_inf(y))
o.value = x.value/y.value; // NaN
else if (is_inf(y))
o.value = x.value;
else
o.value = fmod(x.value, y.value);
// Here is an x87 alternative if the above makes problems; this may also be faster.
#if 0 #if 0
// Here is an x87 alternative if the above makes problems; this may also be faster.
double xv = x.value; double xv = x.value;
double yv = y.value; double yv = y.value;
double & ov = o.value; double & ov = o.value;