diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index 808f4e3dc..c04ed5e8c 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -126,6 +126,40 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const *
     return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
+// ax + by < k
+// <=>
+// -ax - by >= -k + 1
+// <=>
+// a(1-x) + b(1-y) >= -k + a + b + 1
+app * pb_util::mk_lt(unsigned num_args, rational const * _coeffs, expr * const * _args, rational const& _k) {
+    vector<rational> coeffs;
+    rational k(_k);
+    expr_ref_vector args(m);
+    expr* f;
+    rational d(denominator(k));
+    for (unsigned i = 0; i < num_args; ++i) {
+        coeffs.push_back(_coeffs[i]);
+        d = lcm(d, denominator(coeffs[i]));
+        if (m.is_not(_args[i], f)) {
+            args.push_back(f);
+        }
+        else {
+            args.push_back(m.mk_not(f));
+        }
+    }
+    if (!d.is_one()) {
+        k *= d;
+        for (unsigned i = 0; i < num_args; ++i) {
+            coeffs[i] *= d;        
+        }
+    }
+    k.neg();
+    k += rational::one();
+    for (unsigned i = 0; i < num_args; ++i) {
+        k += coeffs[i];
+    }
+    return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k);
+}
 
 
 app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k) {
diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 54da51775..8ecf0f259 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -86,6 +86,7 @@ public:
     app * mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
     app * mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
     app * mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
+    app * mk_lt(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k);
     bool is_at_most_k(func_decl *a) const;
     bool is_at_most_k(expr *a) const { return is_app(a) && is_at_most_k(to_app(a)->get_decl()); }
     bool is_at_most_k(expr *a, rational& k) const;
@@ -106,6 +107,8 @@ public:
     bool is_eq(func_decl* f) const;
     bool is_eq(expr* e) const { return is_app(e) && is_eq(to_app(e)->get_decl()); }
     bool is_eq(expr* e, rational& k) const;
+
+
 private:
     rational to_rational(parameter const& p) const;
 };
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index 282cc03e5..e2cac1d89 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -116,6 +116,15 @@ namespace opt {
             // if (m_bvsls) m_bvsls->display(out);
         }
 
+        void opt(model_ref& mdl) {
+            if (m_engine == symbol("pb")) {
+                pbsls_opt(mdl);
+            }
+            else {
+                bvsls_opt(mdl);
+            }
+        }
+
     protected:
         typedef bvsls_opt_engine::optimization_result opt_result;
 
@@ -123,12 +132,7 @@ namespace opt {
             lbool r = m_solver->check_sat(num_assumptions, assumptions);
             if (r == l_true) {
                 m_solver->get_model(m_model);
-                if (m_engine == symbol("pb")) {
-                    pbsls_opt();
-                }
-                else {
-                    bvsls_opt();
-                }
+                opt(m_model);
             }
             return r;
         }
@@ -191,7 +195,7 @@ namespace opt {
             }
         }
 
-        void pbsls_opt() {
+        void pbsls_opt(model_ref& mdl) {
             #pragma omp critical (sls_solver)
             {
                 if (m_pbsls) {
@@ -201,7 +205,7 @@ namespace opt {
                     m_pbsls = alloc(smt::pb_sls, m);
                 }
             }
-            m_pbsls->set_model(m_model);
+            m_pbsls->set_model(mdl);
             m_pbsls->updt_params(m_params);
             for (unsigned i = 0; i < m_solver->get_num_assertions(); ++i) {
                 m_pbsls->add(m_solver->get_assertion(i));
@@ -213,7 +217,7 @@ namespace opt {
             m_pbsls->get_model(m_model);            
         }
 
-        void bvsls_opt() {
+        void bvsls_opt(model_ref& mdl) {
             #pragma omp critical (sls_solver)
             {
                 m_bvsls = alloc(bvsls_opt_engine, m, m_params);
@@ -223,7 +227,7 @@ namespace opt {
             opt_result res(m);
             res.is_sat = l_undef;
             try {
-                res = m_bvsls->optimize(objective, m_model, true);
+                res = m_bvsls->optimize(objective, mdl, true);
             }
             catch (...) {
                 
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index cd4e167dc..23c1a59b2 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -43,8 +43,10 @@ namespace opt {
         m_dump_benchmarks(false),
         m_fm(alloc(filter_model_converter, m)) {
         m_logic = l;
-        if (m_logic != symbol::null)
+        if (m_logic != symbol::null) {
             m_context.set_logic(m_logic);
+        }
+        m_params.updt_params(p);
         m_params.m_relevancy_lvl = 0;
     }
 
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index b56e28579..fbd028338 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -66,7 +66,10 @@ namespace opt {
         maxsmt_solver_base(solver* s, ast_manager& m): 
             m_s(s), m(m), m_cancel(false), m_soft(m),
             m_enable_sls(false), m_enable_sat(false),
-            m_sls_enabled(false), m_sat_enabled(false) {}
+            m_sls_enabled(false), m_sat_enabled(false) {
+            m_s->get_model(m_model);
+            SASSERT(m_model);
+        }
 
         virtual ~maxsmt_solver_base() {}
         virtual rational get_lower() const { return m_lower; }
@@ -173,9 +176,11 @@ namespace opt {
             if (m_enable_sls && !m_sls_enabled && probe_bv()) {
                 m_params.set_uint("restarts", 20);
                 unsigned lvl = m_s->get_scope_level();
-                m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
+                sls_solver* sls = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
+                m_s = sls;
                 while (lvl > 0) { m_s->push(); --lvl; }
                 m_sls_enabled = true;
+                sls->opt(m_model);
             }
         }
         
@@ -598,9 +603,21 @@ namespace opt {
                 }
             }
             lbool is_sat = l_true;
-            bool was_sat = false;
-            fml = m.mk_true();
             while (l_true == is_sat) {
+                IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";);
+                m_upper.reset();
+                for (unsigned i = 0; i < m_soft.size(); ++i) {
+                    VERIFY(m_model->eval(nsoft[i].get(), val));
+                    TRACE("opt", tout << "eval " << mk_pp(m_soft[i].get(), m) << " " << val << "\n";);
+                    m_assignment[i] = !m.is_true(val);
+                    if (!m_assignment[i]) {
+                        m_upper += m_weights[i];
+                    }
+                }                     
+                TRACE("opt", tout << "new upper: " << m_upper << "\n";);
+                
+                fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
+
                 TRACE("opt", s().display(tout<<"looping\n"););
                 solver::scoped_push _scope2(s());
                 s().assert_expr(fml);
@@ -609,24 +626,10 @@ namespace opt {
                     is_sat = l_undef;
                 }
                 if (is_sat == l_true) {
-                    m_upper.reset();
                     s().get_model(m_model);
-                    for (unsigned i = 0; i < m_soft.size(); ++i) {
-                        VERIFY(m_model->eval(nsoft[i].get(), val));
-                        TRACE("opt", tout << "eval " << mk_pp(m_soft[i].get(), m) << " " << val << "\n";);
-                        m_assignment[i] = !m.is_true(val);
-                        if (!m_assignment[i]) {
-                            m_upper += m_weights[i];
-                        }
-                    }                     
-                    TRACE("opt", tout << "new upper: " << m_upper << "\n";);
-                    IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb solve with upper bound: " << m_upper << ")\n";);
-                    
-                    fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
-                    was_sat = true;
                 }
             }            
-            if (is_sat == l_false && was_sat) {
+            if (is_sat == l_false) {
                 is_sat = l_true;
                 m_lower = m_upper;
             }
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 96ee7f5fc..3dec59d29 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -44,7 +44,7 @@ def_module_params(module_name='smt',
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
                           ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),   
-                          ('pb.conflict_frequency', UINT, 0, 'conflict frequency for Pseudo-Boolean theory'),
+                          ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                           ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),
                           ('pb.enable_simplex', BOOL, False, 'enable simplex to check rational feasibility'),
diff --git a/src/smt/params/theory_pb_params.h b/src/smt/params/theory_pb_params.h
index f6debea8a..0432ac633 100644
--- a/src/smt/params/theory_pb_params.h
+++ b/src/smt/params/theory_pb_params.h
@@ -28,7 +28,7 @@ struct theory_pb_params {
     bool     m_pb_enable_compilation;
     bool     m_pb_enable_simplex;
     theory_pb_params(params_ref const & p = params_ref()):
-        m_pb_conflict_frequency(0),
+        m_pb_conflict_frequency(1000),
         m_pb_learn_complements(true),
         m_pb_enable_compilation(true),
         m_pb_enable_simplex(false)
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index f836a31c4..d933a5f43 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -790,7 +790,6 @@ namespace smt {
     }
 
     void setup::setup_card() {
-        // m_context.register_plugin(alloc(theory_card, m_manager));
         m_context.register_plugin(alloc(theory_pb, m_manager, m_params));
     }
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index fa9810fc5..495c757fa 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -187,8 +187,6 @@ namespace smt {
             m_args[1].append(m_args[0]);
             m_args[1].negate();
             
-            //m_args[0].display(std::cout);
-            //m_args[1].display(std::cout);
             SASSERT(m_args[0].size() == m_args[1].size());
             SASSERT(m_args[0].well_formed());
             SASSERT(m_args[1].well_formed());
@@ -284,8 +282,6 @@ namespace smt {
             m_last_explain(last_explain) {}
 
         virtual void undo(context& ctx) {
-            //std::cout << "undo bound: " << m_v << " " << m_last_explain;
-            //std::cout << (m_is_lower?" lower ":" upper ") << pb.m_mpq_inf_mgr.to_string(m_last_bound) << "\n";
             if (m_is_lower) {
                 if (m_last_bound_valid) {
                     pb.m_simplex.set_lower(m_v, m_last_bound);
@@ -318,7 +314,6 @@ namespace smt {
     }
 
     bool theory_pb::update_bound(bool_var v, literal explain, bool is_lower, mpq_inf const& bound) {
-        // std::cout << v << " " << explain << (is_lower?" lower ":" upper ") << m_mpq_inf_mgr.to_string(bound) << "\n";
         if (is_lower) {
             if (m_simplex.above_lower(v, bound)) {
                 scoped_eps_numeral last_bound(m_mpq_inf_mgr);
@@ -411,6 +406,7 @@ namespace smt {
     }
 
     bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
+        ast_manager& m = get_manager();
         SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || 
                 m_util.is_ge(atom) || m_util.is_at_least_k(atom) || 
                 m_util.is_eq(atom));
@@ -423,7 +419,6 @@ namespace smt {
         SASSERT(!ctx.b_internalized(atom));
         m_stats.m_num_predicates++;
 
-        ast_manager& m = get_manager();
         unsigned num_args = atom->get_num_args();
         bool_var abv = ctx.mk_bool_var(atom);
         ctx.set_var_theory(abv, get_id());