From 659be6940ba4108b82ed9af3f2734e9c95e9aa21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jul 2019 18:01:26 -0400 Subject: [PATCH] fix #2395 Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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());