From 9601761a6febf5f59094610ddabf06f4e5cc589d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 22:12:15 +0100 Subject: [PATCH] Added missing float conversion in fpa2bv converter. Relates to #1178. --- src/ast/fpa/fpa2bv_converter.cpp | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index c84b2a691..c45625513 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2714,13 +2714,21 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con SASSERT(m_util.is_bv2rm(args[0])); expr * bv_rm = to_app(args[0])->get_arg(0); - rational q; - if (!m_arith_util.is_numeral(args[1], q)) - UNREACHABLE(); + SASSERT((m_arith_util.is_int(args[1]) && m_arith_util.is_real(args[2])) || + (m_arith_util.is_real(args[1]) && m_arith_util.is_int(args[2]))); - rational e; - if (!m_arith_util.is_numeral(args[2], e)) - UNREACHABLE(); + rational q, e; + + if (m_arith_util.is_int(args[1]) && m_arith_util.is_real(args[2])) { + if (!m_arith_util.is_numeral(args[1], e) || + !m_arith_util.is_numeral(args[2], q)) + UNREACHABLE(); + } + else { + if (!m_arith_util.is_numeral(args[2], e) || + !m_arith_util.is_numeral(args[1], q)) + UNREACHABLE(); + } SASSERT(e.is_int64()); SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));