From 65a202873f2851b79cb0d498b5714be56e48d8a3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Oct 2013 15:38:54 +0100 Subject: [PATCH] Bugfix for equality rewriting on floats. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 4f8c90301..6ef147f1c 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -490,7 +490,11 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_util.fm()), v2(m_util.fm()); if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) { - result = (v1 == v2) ? m().mk_true() : m().mk_false(); + // Note: == is the floats-equality, here we need normal equality. + result = (m_fm.is_nan(v1) && m_fm.is_nan(v2)) ? m().mk_true() : + (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1)!=m_fm.sgn(v2)) ? m().mk_false() : + (v1 == v2) ? m().mk_true() : + m().mk_false(); return BR_DONE; }