diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 2f7d33f4e..34d586a93 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8883,7 +8883,7 @@ def _pb_args_coeffs(args, default_ctx=None):
     for i in range(len(coeffs)):
         _z3_check_cint_overflow(coeffs[i], "coefficient")
         _coeffs[i] = coeffs[i]
-    return ctx, sz, _args, _coeffs
+    return ctx, sz, _args, _coeffs, args
 
 
 def PbLe(args, k):
@@ -8893,7 +8893,7 @@ def PbLe(args, k):
     >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
     """
     _z3_check_cint_overflow(k, "k")
-    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
+    ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 
@@ -8904,7 +8904,7 @@ def PbGe(args, k):
     >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
     """
     _z3_check_cint_overflow(k, "k")
-    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
+    ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 
@@ -8915,7 +8915,7 @@ def PbEq(args, k, ctx=None):
     >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
     """
     _z3_check_cint_overflow(k, "k")
-    ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
+    ctx, sz, _args, _coeffs, args = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 
diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 71722c7d0..f46f1657c 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -33,11 +33,9 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
                                          unsigned arity, sort * const * domain, sort * range) {
     SASSERT(m_manager);
     ast_manager& m = *m_manager;
-    for (unsigned i = 0; i < arity; ++i) {
-        if (!m.is_bool(domain[i])) {
+    for (unsigned i = 0; i < arity; ++i) 
+        if (!m.is_bool(domain[i])) 
             m.raise_exception("invalid non-Boolean sort applied to 'at-most'");
-        }
-    }
     symbol sym;
     switch(k) {
     case OP_AT_LEAST_K: sym = m_at_least_sym; break;
@@ -50,9 +48,8 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     switch(k) {
     case OP_AT_LEAST_K:
     case OP_AT_MOST_K: {
-        if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) {
+        if (num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) 
             m.raise_exception("function expects one non-negative integer parameter");
-        }
         func_decl_info info(m_family_id, k, 1, parameters);
         return m.mk_func_decl(sym, arity, domain, m.mk_bool_sort(), info);
     }