From 28bdda326ba3ffd54cfb1f111bdbabbce3616a14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Mar 2020 13:36:58 -0700 Subject: [PATCH] fix #3499 Signed-off-by: Nikolaj Bjorner --- src/ast/fpa/fpa2bv_converter.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8c4465391..e1f06e4b2 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -461,6 +461,9 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, big_d_sig = m_bv_util.mk_concat(d_sig, m_bv_util.mk_numeral(0, sbits+3)); SASSERT(is_well_sorted(m, big_d_sig)); + if (ebits > sbits) + throw default_exception("there is no floating point support for division for representations with non-standard bit representations"); + expr_ref shifted_big(m), shifted_d_sig(m), sticky_raw(m), sticky(m); shifted_big = m_bv_util.mk_bv_lshr(big_d_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+3))-ebits), exp_delta));