diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index 8fccb157d..d1714b794 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -801,7 +801,7 @@ struct pb2bv_rewriter::imp {
                 case OP_NUM:
                     VERIFY(au.is_numeral(a, r));
                     m_k -= mul * r;
-                    return true;
+                    return m_k.is_int();
                 case OP_MUL:
                     if (sz != 2) {
                         return false;
@@ -832,7 +832,7 @@ struct pb2bv_rewriter::imp {
                     m_coeffs.push_back(r1-r2);
                     m_k -= r2;
                 }
-                return true;
+                return m_k.is_int();
             }
             return false;
         }