mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

bugfix for hwf::fma

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-22 11:39:28 +01:00
parent 705ace6f0a
commit 759d9f2dda
1 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/util/hwf.cpp
View file

@ -315,11 +315,8 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co
set_rounding_mode(rm); set_rounding_mode(rm);
o.value = x.value * y.value + z.value; o.value = x.value * y.value + z.value;
#else #else
// NOT_IMPLEMENTED_YET(); set_rounding_mode(rm);
// Just a dummy for now: o.value = ::fma(x.value, y.value, z.value);
hwf t;
mul(rm, x, y, t);
add(rm, t, z, o);
#endif #endif
} }