diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 7657fb347..ab2217e13 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -90,6 +90,9 @@ def _z3_assert(cond, msg):
     if not cond:
         raise Z3Exception(msg)
 
+def _z3_check_cint_overflow(n, name):
+    _z3_assert(ctypes.c_int(n).value == n, name + " is too large")
+
 def open_log(fname):
     """Log interaction to a file. This function must be invoked immediately after init(). """
     Z3_open_log(fname)
@@ -8128,6 +8131,7 @@ def _pb_args_coeffs(args, default_ctx = None):
     _args, sz = _to_ast_array(args)
     _coeffs = (ctypes.c_int * len(coeffs))()
     for i in range(len(coeffs)):
+        _z3_check_cint_overflow(coeffs[i], "coefficient")
         _coeffs[i] = coeffs[i]
     return ctx, sz, _args, _coeffs
 
@@ -8137,6 +8141,7 @@ def PbLe(args, k):
     >>> a, b, c = Bools('a b c')
     >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
     """
+    _z3_check_cint_overflow(k, "k")
     ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
@@ -8146,6 +8151,7 @@ def PbGe(args, k):
     >>> a, b, c = Bools('a b c')
     >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
     """
+    _z3_check_cint_overflow(k, "k")
     ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
@@ -8155,6 +8161,7 @@ def PbEq(args, k, ctx = None):
     >>> a, b, c = Bools('a b c')
     >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
     """
+    _z3_check_cint_overflow(k, "k")
     ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)