diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index b35b9f683..cb25ecad6 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -134,8 +134,8 @@ app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const *
         all_ones &= m_coeffs[i].is_one();
         m_params.push_back(parameter(m_coeffs[i]));
     }
-    if (all_ones && k.is_unsigned()) {
-        m_params[0] = parameter(floor(m_k).get_unsigned());
+    if (all_ones && k.is_unsigned() && floor(m_k).is_int32()) {
+        m_params[0] = parameter(floor(m_k).get_int32());
         return m.mk_app(m_fid, OP_AT_MOST_K, 1, m_params.c_ptr(), num_args, args, m.mk_bool_sort());
     }
     return m.mk_app(m_fid, OP_PB_LE, m_params.size(), m_params.c_ptr(), num_args, args, m.mk_bool_sort());