diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 2c33bd955..5e1febe9e 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1065,13 +1065,14 @@ namespace sat {
         return c;
     }
 
-    void ba_solver::get_coeff(bool_var v, literal& l, unsigned& c) {
+    ba_solver::wliteral ba_solver::get_wliteral(bool_var v) {
         int64_t c1 = get_coeff(v);
-        l = literal(v, c1 < 0);
+        literal l = literal(v, c1 < 0);
         c1 = std::abs(c1);
-        c = static_cast<unsigned>(c1);
+        unsigned c = static_cast<unsigned>(c1);
         // TRACE("ba", tout << l << " " << c << "\n";);
         m_overflow |= c != c1;
+        return wliteral(c, l);
     }
 
     unsigned ba_solver::get_abs_coeff(bool_var v) const {
@@ -1121,7 +1122,6 @@ namespace sat {
 // #define DEBUG_CODE(_x_) _x_
 
     void ba_solver::bail_resolve_conflict(unsigned idx) {
-        m_overflow = false;
         literal_vector const& lits = s().m_trail;
         while (m_num_marks > 0) {
             bool_var v = lits[idx].var();
@@ -1157,13 +1157,14 @@ namespace sat {
     }
 
     lbool ba_solver::resolve_conflict() { 
-#if 1
-        return resolve_conflict_rs();
-#endif
-       
         if (0 == m_num_propagations_since_pop) {
             return l_undef;
         }
+
+        if (s().m_config.m_pb_resolve == PB_ROUNDING) {
+            return resolve_conflict_rs();
+        }
+       
         m_overflow = false;
         reset_coeffs();
         m_num_marks = 0;
@@ -1348,6 +1349,10 @@ namespace sat {
         return l_true;
 
     bail_out:
+        if (m_overflow) {
+            ++m_stats.m_num_overflow;
+            m_overflow = false;
+        }
         bail_resolve_conflict(idx);
         return l_undef;
     }
@@ -1403,24 +1408,25 @@ namespace sat {
             }
         }
         ineq.divide(c);
+        TRACE("ba", display(tout << "var: " << v << " " << c << ": ", ineq, true););
     }
 
     void ba_solver::round_to_one(bool_var w) {
         unsigned c = get_abs_coeff(w);
         if (c == 1 || c == 0) return;
         for (bool_var v : m_active_vars) {
-            literal l;
-            unsigned ci;
-            get_coeff(v, l, ci);
-            unsigned q = ci % c;
-            if (q != 0 && !is_false(l)) {
-                m_coeffs[v] = ci - q;
+            wliteral wl = get_wliteral(v);
+            unsigned q = wl.first % c;
+            if (q != 0 && !is_false(wl.second)) {
+                m_coeffs[v] = wl.first - q;
                 m_bound -= q;
                 SASSERT(m_bound > 0);
             }
         }        
+        SASSERT(validate_lemma());
         divide(c);
         SASSERT(validate_lemma());
+        TRACE("ba", active2pb(m_B); display(tout, m_B, true););
     }
 
     void ba_solver::divide(unsigned c) {
@@ -1431,8 +1437,7 @@ namespace sat {
         for (unsigned i = 0; i < sz; ++i) {
             bool_var v = m_active_vars[i];
             int ci = get_int_coeff(v);
-            if (m_active_var_set.contains(v) || ci == 0) continue;
-            m_active_var_set.insert(v);
+            if (!test_and_set_active(v) || ci == 0) continue;
             if (ci > 0) {
                 m_coeffs[v] = (ci + c - 1) / c;
             }
@@ -1452,10 +1457,13 @@ namespace sat {
 
     void ba_solver::resolve_with(ineq const& ineq) {
         TRACE("ba", display(tout, ineq, true););
-        inc_bound(ineq.m_k);
+        inc_bound(ineq.m_k);        
+        TRACE("ba", tout << "bound: " << m_bound << "\n";);
+
         for (unsigned i = ineq.size(); i-- > 0; ) {
             literal l = ineq.lit(i);
             inc_coeff(l, static_cast<unsigned>(ineq.coeff(i)));
+            TRACE("ba", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";);
         }
     }
 
@@ -1518,27 +1526,26 @@ namespace sat {
             switch (js.get_kind()) {
             case justification::NONE:
                 SASSERT(consequent != null_literal);
-                inc_bound(1);
                 round_to_one(consequent.var());
+                inc_bound(1);
                 inc_coeff(consequent, 1);
                 break;
             case justification::BINARY:
                 SASSERT(consequent != null_literal);
-                inc_bound(1);
                 round_to_one(consequent.var());
+                inc_bound(1);
                 inc_coeff(consequent, 1);
                 process_antecedent(js.get_literal());
                 break;
             case justification::TERNARY:
                 SASSERT(consequent != null_literal);
-                inc_bound(1);
                 round_to_one(consequent.var());
+                inc_bound(1);
                 inc_coeff(consequent, 1);
                 process_antecedent(js.get_literal1());
                 process_antecedent(js.get_literal2());
                 break;
             case justification::CLAUSE: {
-                inc_bound(1);
                 clause & c = s().get_clause(js);
                 unsigned i = 0;
                 if (consequent != null_literal) {
@@ -1553,6 +1560,7 @@ namespace sat {
                         i = 2;
                     }
                 }
+                inc_bound(1);
                 unsigned sz = c.size();
                 for (; i < sz; i++)
                     process_antecedent(c[i]);
@@ -1576,6 +1584,7 @@ namespace sat {
                         }
                         else {
                             SASSERT(k > c);
+                            TRACE("ba", tout << "visited: " << l << "\n";);
                             k -= c;
                         }
                     }
@@ -1590,6 +1599,7 @@ namespace sat {
                 }
                 mark_variables(m_A);
                 if (consequent == null_literal) {
+                    SASSERT(validate_ineq(m_A)); 
                     m_bound = static_cast<unsigned>(m_A.m_k);
                     for (wliteral wl : m_A.m_wlits) {
                         process_antecedent(wl.second, wl.first);
@@ -1597,9 +1607,11 @@ namespace sat {
                 }
                 else {
                     round_to_one(consequent.var());
-                    if (cnstr.tag() == pb_t) round_to_one(m_A, consequent.var());  
+                    if (cnstr.tag() == pb_t) round_to_one(m_A, consequent.var()); 
+                    SASSERT(validate_ineq(m_A)); 
                     resolve_with(m_A);
                 }
+                break;
             }
             default:
                 UNREACHABLE();
@@ -1616,13 +1628,18 @@ namespace sat {
                 v = consequent.var();
                 mark_visited(v);
                 if (s().is_marked(v)) {
-                    if (get_coeff(v) != 0) {
+                    int64_t c = get_coeff(v);
+                    if (c == 0) {
+                        CTRACE("ba", c != 0, active2pb(m_A); display(tout << consequent << ": ", m_A, true););
+                        s().reset_mark(v);
+                        --m_num_marks;
+                    }
+                    else {
                         break;
                     }
-                    s().reset_mark(v);
-                    --m_num_marks;
                 }
                 if (idx == 0) {
+                    TRACE("ba", tout << "there is no consequent\n";);
                     goto bail_out;
                 }
                 --idx;
@@ -1647,9 +1664,14 @@ namespace sat {
             active2constraint();
             return l_true;
         }
+        
     bail_out:
-        IF_VERBOSE(1, verbose_stream() << "bail\n");
-        m_overflow = false;
+        IF_VERBOSE(1, verbose_stream() << "bail " << m_overflow << "\n");
+        TRACE("ba", tout << "bail " << m_overflow << "\n";);
+        if (m_overflow) {
+            ++m_stats.m_num_overflow;
+            m_overflow = false;
+        }
         return l_undef;
     }
 
@@ -1657,9 +1679,16 @@ namespace sat {
     bool ba_solver::create_asserting_lemma() {
         int64_t bound64 = m_bound;
         int64_t slack = -bound64;
-        for (bool_var v : m_active_vars) {
-            slack += get_abs_coeff(v);
+        reset_active_var_set();
+        unsigned j = 0, sz = m_active_vars.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            bool_var v = m_active_vars[i];
+            unsigned c = get_abs_coeff(v);
+            if (!test_and_set_active(v) || c == 0) continue;
+            slack += c;
+            m_active_vars[j++] = v;
         }
+        m_active_vars.shrink(j);
         m_lemma.reset();        
         m_lemma.push_back(null_literal);
         unsigned num_skipped = 0;
@@ -1694,16 +1723,19 @@ namespace sat {
             }
         }
         if (slack >= 0) {
+            TRACE("ba", tout << "slack is non-negative\n";);
             IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
             return false;
         }
         if (m_overflow) {
+            TRACE("ba", tout << "overflow\n";);
             return false;
         }        
         if (m_lemma[0] == null_literal) {
             if (m_lemma.size() == 1) {
                 s().set_conflict(justification());
             }
+            TRACE("ba", tout << "no asserting literal\n";);
             return false;
         }
 
@@ -1767,8 +1799,7 @@ namespace sat {
             for (unsigned i = 0; i < sz; ++i) {
                 bool_var v = m_active_vars[i];
                 int64_t c = m_coeffs[v];
-                if (m_active_var_set.contains(v) || c == 0) continue;
-                m_active_var_set.insert(v);
+                if (!test_and_set_active(v) || c == 0) continue;
                 m_coeffs[v] /= static_cast<int>(g);
                 m_active_vars[j++] = v;
             }
@@ -1834,7 +1865,8 @@ namespace sat {
         return p;        
     }
 
-    ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) {        
+    ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), 
+                            m_allocator("ba"), m_constraint_id(0), m_ba(*this), m_sort(m_ba) {        
         TRACE("ba", tout << this << "\n";);
         m_num_propagations_since_pop = 0;
     }
@@ -2649,8 +2681,12 @@ namespace sat {
             constraint* c = m_learned[i];
             if (!m_constraint_to_reinit.contains(c)) {
                 remove_constraint(*c, "gc");
+                m_allocator.deallocate(c->obj_size(), c);
                 ++removed;
             }
+            else {
+                m_learned[new_sz++] = c;
+            }
         }
         m_stats.m_num_gc += removed;
         m_learned.shrink(new_sz);
@@ -3453,38 +3489,58 @@ namespace sat {
         }
     }
 
-    void ba_solver::unit_strengthen(big& big, card& c) {
-        for (literal l : c) {
-            literal r = big.get_root(~l);
-            if (r == ~l) continue;
-            unsigned k = c.k();
-            for (literal u : c) {
-                if (big.reaches(r, ~u)) {
-                    if (k == 0) {
-                        // ~r + C >= c.k() + 1
-                        IF_VERBOSE(0, verbose_stream() << "TBD add " << ~r << " to " << c << "\n";);
-                        return;
-                    }
-                    --k;                    
+    void ba_solver::unit_strengthen(big& big, pb_base& p) {
+        if (p.lit() != null_literal) return;
+        unsigned sz = p.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            literal u = p.get_lit(i);
+            literal r = big.get_root(u);
+            if (r == u) continue;
+            unsigned k = p.k(), b = 0;
+            for (unsigned j = 0; j < sz; ++j) {
+                literal v = p.get_lit(j);
+                if (r == big.get_root(v)) {
+                    b += p.get_coeff(j);
                 }
-            }
-        }
-    }
-
-    void ba_solver::unit_strengthen(big& big, pb& p) {
-        for (wliteral wl : p) {
-            literal r = big.get_root(~wl.second);
-            if (r == ~wl.second) continue;
-            unsigned k = p.k();
-            for (wliteral u : p) {
-                if (big.reaches(r, ~u.second)) {
-                    if (k < u.first) {
-                        // ~r + p >= p.k() + 1
-                        IF_VERBOSE(0, verbose_stream() << "TBD add " << ~r << " to " << p << "\n";);
-                        return;
+            }            
+            if (b > k) {
+                r.neg();
+                unsigned coeff = b - k;
+                
+                svector<wliteral> wlits;
+                // add coeff * r to p
+                wlits.push_back(wliteral(coeff, r));
+                for (unsigned j = 0; j < sz; ++j) {
+                    u = p.get_lit(j);
+                    unsigned c = p.get_coeff(j);
+                    if (r == u) {
+                        wlits[0].first += c;
+                    }
+                    else if (~r == u) {
+                        if (coeff == c) {
+                            wlits[0] = wlits.back();
+                            wlits.pop_back();
+                            b -= c;
+                        }
+                        else if (coeff < c) {
+                            wlits[0].first = c - coeff;
+                            wlits[0].second.neg();
+                            b -= coeff;
+                        }
+                        else {
+                            // coeff > c
+                            wlits[0].first = coeff - c;
+                            b -= c;
+                        }
+                    }
+                    else {
+                        wlits.push_back(wliteral(c, u));
                     }
-                    k -= u.first;
                 }
+                ++m_stats.m_num_big_strengthenings;
+                p.set_removed();
+                constraint* c = add_pb_ge(null_literal, wlits, b, p.learned());
+                return;
             }
         }
     }
@@ -3784,7 +3840,7 @@ namespace sat {
         }
         init_visited();
         for (wliteral l : p1) {
-            SASSERT(m_weights[l.second.index()] == 0);
+            SASSERT(m_weights.get(l.second.index(), 0) == 0);
             m_weights.setx(l.second.index(), l.first, 0);
             mark_visited(l.second);  
         }
@@ -3992,7 +4048,8 @@ namespace sat {
 
     void ba_solver::display(std::ostream& out, ineq const& ineq, bool values) const {
         for (unsigned i = 0; i < ineq.size(); ++i) {
-            out << ineq.coeff(i) << "*" << ineq.lit(i) << " ";
+            if (ineq.coeff(i) != 1) out << ineq.coeff(i) << "*";
+            out << ineq.lit(i) << " ";
             if (values) out << value(ineq.lit(i)) << " ";
         }
         out << ">= " << ineq.m_k << "\n";
@@ -4083,6 +4140,8 @@ namespace sat {
         st.update("ba resolves", m_stats.m_num_resolves);
         st.update("ba cuts", m_stats.m_num_cut);
         st.update("ba gc", m_stats.m_num_gc);
+        st.update("ba overflow", m_stats.m_num_overflow);
+        st.update("ba big strengthenings", m_stats.m_num_big_strengthenings);
     }
 
     bool ba_solver::validate_unit_propagation(card const& c, literal alit) const { 
@@ -4177,23 +4236,44 @@ namespace sat {
         int64_t val = -bound64;
         reset_active_var_set();
         for (bool_var v : m_active_vars) {
-            if (m_active_var_set.contains(v)) continue;            
-            unsigned coeff;
-            literal lit;
-            get_coeff(v, lit, coeff);
-            if (coeff == 0) continue;
-            if (!is_false(lit)) {
-                val += coeff;
+            if (!test_and_set_active(v)) continue;
+            wliteral wl = get_wliteral(v);
+            if (wl.first == 0) continue;
+            if (!is_false(wl.second)) {
+                val += wl.first;
             }
         }
-        CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A););
+        CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A, true););
         return val < 0;
     }
 
+    /**
+     * the slack of inequalities on the stack should be non-positive.
+     */
+    bool ba_solver::validate_ineq(ineq const& ineq) const {
+        int64_t k = -static_cast<int64_t>(ineq.m_k);
+        for (wliteral wl : ineq.m_wlits) {
+            if (!is_false(wl.second))
+                k += wl.first;
+        }
+        CTRACE("ba", k > 0, display(tout, ineq, true););
+        return k <= 0;
+    }
+
     void ba_solver::reset_active_var_set() {
         while (!m_active_var_set.empty()) m_active_var_set.erase();
     }
 
+    bool ba_solver::test_and_set_active(bool_var v) {
+        if (m_active_var_set.contains(v)) {
+            return false;
+        }
+        else {
+            m_active_var_set.insert(v);
+            return true;
+        }
+    }
+
     void ba_solver::active2pb(ineq& p) {
         p.reset(m_bound);
         active2wlits(p.m_wlits);
@@ -4205,17 +4285,14 @@ namespace sat {
     }
 
     void ba_solver::active2wlits(svector<wliteral>& wlits) {
-        reset_active_var_set();
         uint64_t sum = 0;        
+        reset_active_var_set();
         for (bool_var v : m_active_vars) {
-            if (m_active_var_set.contains(v)) continue;
-            unsigned coeff;
-            literal lit;
-            get_coeff(v, lit, coeff);
-            if (coeff == 0) continue;
-            m_active_var_set.insert(v);
-            wlits.push_back(wliteral(coeff, lit));
-            sum += coeff;
+            if (!test_and_set_active(v)) continue;
+            wliteral wl = get_wliteral(v);
+            if (wl.first == 0) continue;
+            wlits.push_back(wl);
+            sum += wl.first;
         }
         m_overflow |= sum >= UINT_MAX/2;
     }
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 9418cdd99..b547c2292 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -42,8 +42,10 @@ namespace sat {
             unsigned m_num_bin_subsumes;
             unsigned m_num_clause_subsumes;
             unsigned m_num_pb_subsumes;
+            unsigned m_num_big_strengthenings;
             unsigned m_num_cut;
             unsigned m_num_gc;
+            unsigned m_num_overflow;
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
@@ -316,8 +318,7 @@ namespace sat {
         bool elim_pure(literal lit);
         void unit_strengthen();
         void unit_strengthen(big& big, constraint& cs);
-        void unit_strengthen(big& big, card& c);
-        void unit_strengthen(big& big, pb& p);
+        void unit_strengthen(big& big, pb_base& p);
         void subsumption(constraint& c1);
         void subsumption(card& c1);
         void gc_half(char const* _method);
@@ -455,10 +456,11 @@ namespace sat {
 
         mutable bool m_overflow;
         void reset_active_var_set();
+        bool test_and_set_active(bool_var v);
         void inc_coeff(literal l, unsigned offset);
         int64_t get_coeff(bool_var v) const;
         uint64_t get_coeff(literal lit) const;
-        void get_coeff(bool_var v, literal& l, unsigned& c);
+        wliteral get_wliteral(bool_var v);
         unsigned get_abs_coeff(bool_var v) const;       
         int   get_int_coeff(bool_var v) const;
         unsigned get_bound() const;
@@ -477,6 +479,7 @@ namespace sat {
         bool validate_conflict(pb const& p) const;
         bool validate_assign(literal_vector const& lits, literal lit);
         bool validate_lemma();
+        bool validate_ineq(ineq const& ineq) const;
         bool validate_unit_propagation(card const& c, literal alit) const;
         bool validate_unit_propagation(pb const& p, literal alit) const;
         bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index c7f2377c9..ad83fac7a 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -196,6 +196,14 @@ namespace sat {
         else 
             throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented");
 
+        s = p.pb_resolve();
+        if (s == "cardinality") 
+            m_pb_resolve = PB_CARDINALITY;
+        else if (s == "rounding") 
+            m_pb_resolve = PB_ROUNDING;
+        else 
+            throw sat_param_exception("invalid PB resolve: 'cardinality' or 'resolve' expected");
+
         m_card_solver = p.cardinality_solver();
 
         sat_simplifier_params sp(_p);
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 37efe69ed..40ab5fa38 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -60,6 +60,11 @@ namespace sat {
         PB_SEGMENTED
     };
 
+    enum pb_resolve {
+        PB_CARDINALITY,
+        PB_ROUNDING
+    };
+
     enum reward_t {
         ternary_reward,
         unit_literal_reward,
@@ -148,6 +153,7 @@ namespace sat {
         
         pb_solver          m_pb_solver;
         bool               m_card_solver;
+        pb_resolve         m_pb_resolve;
         
         // branching heuristic settings.
         branching_heuristic m_branching_heuristic;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 89776c479..7c289a900 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -42,8 +42,9 @@ def_module_params('sat',
                           ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
                           ('cardinality.solver', BOOL, True, 'use cardinality solver'),
                           ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'),
-                          ('xor.solver', BOOL, False, 'use xor solver'),
+                          ('xor.solver', BOOL, False, 'use xor solver'),                        
                           ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
+                          ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
                           ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 7faa89370..9d0d29ac0 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -82,6 +82,7 @@ struct goal2sat::imp {
         m_is_lemma(false) {
         updt_params(p);
         m_true = sat::null_bool_var;
+        mk_true();
     }
         
     void updt_params(params_ref const & p) {
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 0f3715cb1..e6518b435 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -269,10 +269,9 @@ public:
     void remove(unsigned v) {
         if (contains(v)) {
             m_in_set[v] = false;
-            unsigned i = 0;
-            for (i = 0; i < m_set.size() && m_set[i] != v; ++i)
-                ;
-            SASSERT(i < m_set.size());
+            unsigned i = m_set.size();
+            for (; i > 0 && m_set[--i] != v; ) ;
+            SASSERT(m_set[i] == v);
             m_set[i] = m_set.back();
             m_set.pop_back();
         }