mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

FPA: bugfix for corner-case sign of division

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-04-05 15:27:05 +01:00
parent 26efb3c7f1
commit 5915533170
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -711,11 +711,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
mk_is_ninf(y, c5); mk_is_ninf(y, c5);
mk_ite(x_is_inf, nan, xy_zero, v5); mk_ite(x_is_inf, nan, xy_zero, v5);
// (y is 0) -> if (x is 0) then NaN else inf with x's sign. // (y is 0) -> if (x is 0) then NaN else inf with xor sign.
c6 = y_is_zero; c6 = y_is_zero;
expr_ref x_sgn_inf(m); expr_ref sgn_inf(m);
mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); mk_ite(signs_xor, ninf, pinf, sgn_inf);
mk_ite(x_is_zero, nan, x_sgn_inf, v6); mk_ite(x_is_zero, nan, sgn_inf, v6);
// (x is 0) -> result is zero with sgn = x.sgn^y.sgn // (x is 0) -> result is zero with sgn = x.sgn^y.sgn
// This is a special case to avoid problems with the unpacking of zero. // This is a special case to avoid problems with the unpacking of zero.