From 507356c7bf6aa472abb1625a9a24465aeb9c9667 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Jul 2017 20:18:39 +0100 Subject: [PATCH] Fixed bug in fpa2bv converter. Fixes #1178. --- src/ast/fpa/fpa2bv_converter.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 0f4d26739..c84b2a691 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2714,12 +2714,12 @@ 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 e; - if (!m_arith_util.is_numeral(args[1], e)) + rational q; + if (!m_arith_util.is_numeral(args[1], q)) UNREACHABLE(); - rational q; - if (!m_arith_util.is_numeral(args[2], q)) + rational e; + if (!m_arith_util.is_numeral(args[2], e)) UNREACHABLE(); SASSERT(e.is_int64());