From 31e78cd17805c5efa36bbf6c526c466488585264 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 6 May 2015 12:24:18 +0100 Subject: [PATCH] Bugfix for fp.rem(0, 0). Fixes #70. --- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++++------ src/util/mpf.cpp | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 60120bea2..1543ce629 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -959,14 +959,14 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, c3 = y_is_inf; v3 = x; - // (x is 0) -> x - c4 = x_is_zero; - v4 = pzero; - // (y is 0) -> NaN. - c5 = y_is_zero; - v5 = nan; + c4 = y_is_zero; + v4 = nan; + // (x is 0) -> x + c5 = x_is_zero; + v5 = pzero; + // else the actual remainder. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9de56773a..490a8792f 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1099,10 +1099,10 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { mk_nan(x.ebits, x.sbits, o); else if (is_inf(y)) set(o, x); - else if (is_zero(x)) - set(o, x); else if (is_zero(y)) mk_nan(x.ebits, x.sbits, o); + else if (is_zero(x)) + set(o, x); else { o.ebits = x.ebits; o.sbits = x.sbits;