From 5915533170b069e1b74a1e7fe5e14b263a48e299 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 5 Apr 2013 15:27:05 +0100 Subject: [PATCH] FPA: bugfix for corner-case sign of division Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 6d39dbfc4..84a1efaff 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -711,11 +711,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, mk_is_ninf(y, c5); 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; - expr_ref x_sgn_inf(m); - mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); - mk_ite(x_is_zero, nan, x_sgn_inf, v6); + expr_ref sgn_inf(m); + mk_ite(signs_xor, ninf, pinf, sgn_inf); + mk_ite(x_is_zero, nan, sgn_inf, v6); // (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.