From 4d3910880853575a2058670d164a5040df1b8a81 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Sep 2015 12:21:59 +0100 Subject: [PATCH] Bugfix for fp.to_sbv Fixes #162 --- src/ast/fpa/fpa2bv_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 906327ecc..20c4822d2 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2876,7 +2876,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args else c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift), m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift), - m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sbits-1))))); + m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1))))); dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits); expr_ref r_shifted_sig(m), l_shifted_sig(m);