mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Add missing assertion. Fixes #4642.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-10-30 14:09:51 +00:00
parent 1730bc7c7f
commit c03c395267
No known key found for this signature in database
GPG key ID: BCF6360F86294467
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/util/mpf.cpp
View file

@ -745,7 +745,8 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf &
}
void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf const &z, mpf & o) {
SASSERT(x.sbits == y.sbits && x.ebits == y.ebits);
SASSERT(x.sbits == y.sbits && x.ebits == y.ebits &&
x.sbits == z.sbits && x.ebits == z.ebits);
TRACE("mpf_dbg", tout << "X = " << to_string(x) << std::endl;);
TRACE("mpf_dbg", tout << "Y = " << to_string(y) << std::endl;);