mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

Bugfix for special-case handling in fp.fma.

Browse source 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
This commit is contained in:
Christoph M. Wintersteiger 2016-12-09 15:03:31 +00:00
parent 56b1a8b086
commit 16b32ecf12
2 changed files with 24 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_model_checker.cpp
View file

@ -295,7 +295,6 @@ namespace smt {
break;
model_ref cex;
m_aux_context->get_model(cex);
TRACE("model_checker", tout << "[restricted] model-checker model cex:\n"; model_pp(tout, *cex););
if (!add_instance(q, cex.get(), sks, true)) {
break;
}

5
src/util/mpf.cpp
View file

@ -795,8 +795,9 @@ void mpf_manager::fma(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf co
set(o, z);
}
else if (is_zero(x) || is_zero(y)) {
if (is_zero(z) && rm != MPF_ROUND_TOWARD_NEGATIVE)
mk_pzero(x.ebits, x.sbits, o);
bool xy_sgn = is_neg(x) ^ is_neg(y);
if (is_zero(z) && xy_sgn ^ is_neg(z))
mk_zero(x.ebits, x.sbits, rm != MPF_ROUND_TOWARD_NEGATIVE, o);
else
set(o, z);
}