diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index e255f4b108..533383484b 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -1091,6 +1091,13 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons
         scoped_mpf sv(fm());
         if (!is_rm_numeral(rm, rmv) || !is_numeral(x, sv)) return false;
         if (is_nan(x) || is_inf(x)) return true;
+        // A finite value whose (unbiased) binary exponent is at least bv_sz has
+        // magnitude >= 2^bv_sz, so it cannot fit into a bv_sz-bit signed or
+        // unsigned integer and the conversion is unspecified. Detect this here to
+        // avoid calling to_sbv_mpq, which rejects exponents that do not fit into
+        // an int (throwing "exponents over 31 bits are not supported").
+        if (plugin().fm().exp(sv) >= (mpf_exp_t)bv_sz)
+            return true;
         unsynch_mpq_manager& mpqm = plugin().fm().mpq_manager();
         scoped_mpq r(mpqm);
         plugin().fm().to_sbv_mpq(rmv, sv, r);
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index c2c888885b..3be70d4057 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -721,6 +721,14 @@ br_status fpa_rewriter::mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool i
         if (m_fm.is_nan(v) || m_fm.is_inf(v))
             return mk_to_bv_unspecified(f, result);
 
+        // A finite value whose (unbiased) binary exponent is at least bv_sz has
+        // magnitude >= 2^bv_sz and therefore does not fit into a bv_sz-bit signed
+        // or unsigned integer; the conversion is unspecified. Handle it here to
+        // avoid calling to_sbv_mpq, which rejects exponents that do not fit into
+        // an int (throwing "exponents over 31 bits are not supported").
+        if (m_fm.exp(v) >= (mpf_exp_t)bv_sz)
+            return mk_to_bv_unspecified(f, result);
+
         bv_util bu(m());
         scoped_mpq q(m_fm.mpq_manager());
         m_fm.to_sbv_mpq(rmv, v, q);