diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 89615e11e..bd954d8ff 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)
@@ -8132,6 +8135,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
 
@@ -8141,6 +8145,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)
 
@@ -8150,6 +8155,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)
 
@@ -8159,6 +8165,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)
 
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 4fbf7570d..669389d2a 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -166,10 +166,11 @@ namespace sat {
         unsigned w = 0;
         for (unsigned i = 0; i < m_size; ++i) {
             m_wlits[i].second.neg();
+            VERIFY(w + m_wlits[i].first >= w);
             w += m_wlits[i].first;
-        }
+        }        
         m_k = w - m_k + 1;
-        SASSERT(w >= m_k && m_k > 0);
+        VERIFY(w >= m_k && m_k > 0);
     }
 
     bool ba_solver::pb::is_watching(literal l) const {
@@ -526,11 +527,13 @@ namespace sat {
     bool ba_solver::init_watch(pb& p) {
         clear_watch(p);        
         if (p.lit() != null_literal && value(p.lit()) == l_false) {
+            //IF_VERBOSE(0, verbose_stream() << "negate: " << p.k() << "\n");
             p.negate();           
         }
         
         VERIFY(p.lit() == null_literal || value(p.lit()) == l_true);
         unsigned sz = p.size(), bound = p.k();
+        //IF_VERBOSE(0, verbose_stream() << "bound: " << p.k() << "\n");
 
         // put the non-false literals into the head.
         unsigned slack = 0, slack1 = 0, num_watch = 0, j = 0;
@@ -833,9 +836,19 @@ namespace sat {
             remove_constraint(p, "recompiled to cardinality");
             return;
         }
-
         else {
             p.set_size(sz);
+            p.update_max_sum();
+            if (p.max_sum() < k) {
+                if (p.lit() == null_literal) {
+                    s().set_conflict(justification());
+                }
+                else {
+                    s().assign(~p.lit(), justification());
+                }
+                remove_constraint(p, "recompiled to false");
+                return;
+            }
             p.set_k(k);
             SASSERT(p.well_formed());
             
@@ -3210,6 +3223,7 @@ namespace sat {
             if (is_marked(l) && m_weights[l.index()] <= p2.get_coeff(i)) {
                 ++num_sub;
             }
+			if (p1.size() + i > p2.size() + num_sub) return false;
         }
         return num_sub == p1.size();
     }
@@ -3364,8 +3378,9 @@ namespace sat {
             m_weights.setx(l.second.index(), l.first, 0);
             mark_visited(l.second);  
         }
-        for (unsigned i = 0; i < p1.num_watch(); ++i) {
-            subsumes(p1, p1[i].second);
+        for (unsigned i = 0; i < std::min(10u, p1.num_watch()); ++i) {
+            unsigned j = s().m_rand() % p1.num_watch();
+            subsumes(p1, p1[j].second);
         }
         for (wliteral l : p1) {
             m_weights[l.second.index()] = 0;
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 07e7cfd58..e947cee96 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -124,8 +124,8 @@ namespace sat {
         protected:
             unsigned       m_k;
         public:
-            pb_base(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): constraint(t, id, l, sz, osz), m_k(k) {}
-            virtual void set_k(unsigned k) { m_k = k; }
+            pb_base(tag_t t, unsigned id, literal l, unsigned sz, size_t osz, unsigned k): constraint(t, id, l, sz, osz), m_k(k) { VERIFY(k < 4000000000); }
+            virtual void set_k(unsigned k) { VERIFY(k < 4000000000);  m_k = k; }
             virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; }
             unsigned k() const { return m_k; }
             virtual bool well_formed() const;
@@ -157,7 +157,6 @@ namespace sat {
             unsigned       m_num_watch;
             unsigned       m_max_sum;
             wliteral       m_wlits[0];
-            void update_max_sum();
         public:
             static size_t get_obj_size(unsigned num_lits) { return sizeof(pb) + num_lits * sizeof(wliteral); }
             pb(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
@@ -171,10 +170,11 @@ namespace sat {
             void set_slack(unsigned s) { m_slack = s; }
             unsigned num_watch() const { return m_num_watch; }
             unsigned max_sum() const { return m_max_sum; }
+            void update_max_sum();
             void set_num_watch(unsigned s) { m_num_watch = s; }
             bool is_cardinality() const;
             virtual void negate();                       
-            virtual void set_k(unsigned k) { m_k = k; update_max_sum(); }
+            virtual void set_k(unsigned k) { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
             virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
             virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
             virtual bool is_watching(literal l) const;