From 2714dc26236919116afd7bf5e98b7b56caa92865 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 May 2025 17:46:51 +0100 Subject: [PATCH] fix #7661 --- src/ast/fpa/fpa2bv_converter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index af4a330f3..f03dcbe1a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2811,7 +2811,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * rational min_real, max_real; const mpz& max_exp_z = m_mpf_manager.m_powers2.m1(ebits-1); - SASSERT(m_mpz_manager.is_uint(max_exp_z)); + if (!m_mpz_manager.is_uint(max_exp_z)) + throw default_exception("exponents requiring more than 32 bits are not supported"); unsigned max_exp = m_mpz_manager.get_uint(max_exp_z); rational max_sig = m_mpf_manager.m_powers2.m1(sbits) / m_mpf_manager.m_powers2(sbits-1); max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp));