diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/contrib/cmake/src/opt/CMakeLists.txt
index 778edc2de..b8d17ec89 100644
--- a/contrib/cmake/src/opt/CMakeLists.txt
+++ b/contrib/cmake/src/opt/CMakeLists.txt
@@ -1,7 +1,6 @@
 z3_add_component(opt
   SOURCES
     maxres.cpp
-    maxsls.cpp
     maxsmt.cpp
     mss.cpp
     opt_cmds.cpp
diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp
deleted file mode 100644
index 4e59cfdfd..000000000
--- a/src/opt/maxsls.cpp
+++ /dev/null
@@ -1,73 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    maxsls.cpp
-
-Abstract:
-
-    Weighted SLS MAXSAT module
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-4-17
-
-Notes:
-
---*/
-
-#include "maxsls.h"
-#include "ast_pp.h"
-#include "model_smt2_pp.h"
-#include "opt_context.h"
-#include "inc_sat_solver.h"
-
-
-namespace opt {
-
-    class sls : public maxsmt_solver_base {
-    public:
-        sls(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
-            maxsmt_solver_base(c, ws, soft) {
-        }
-        virtual ~sls() {}
-        lbool operator()() {
-            IF_VERBOSE(1, verbose_stream() << "(opt.sls)\n";);
-            init();
-            enable_sls(true);
-            lbool is_sat = check();
-            if (is_sat == l_true) {
-                s().get_model(m_model);
-                m_upper.reset();
-                for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    expr_ref tmp(m);
-                    m_model->eval(m_soft[i], tmp, true);
-                    m_assignment[i] = m.is_true(tmp);
-                    if (!m_assignment[i]) {
-                        m_upper += m_weights[i];
-                    }
-                }
-            }
-            return is_sat;
-        }
-        
-        lbool check() {
-            if (m_c.sat_enabled()) {
-                return inc_sat_check_sat(
-                    s(), m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr(), m_upper);
-            }
-            else {
-                return s().check_sat(0, 0);
-            }
-        }
-
-    };
-
-    maxsmt_solver_base* mk_sls(
-        maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
-        return alloc(sls, c, ws, soft);
-    }
-
-
-};
diff --git a/src/opt/maxsls.h b/src/opt/maxsls.h
deleted file mode 100644
index b23512df4..000000000
--- a/src/opt/maxsls.h
+++ /dev/null
@@ -1,35 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    maxsls.h
-
-Abstract:
-
-    Weighted SLS MAXSAT module
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-4-17
-
-Notes:
-
-    Partial, one-round SLS optimizer. Finds the first 
-    local maximum given a resource bound and returns.
-
---*/
-#ifndef OPT_SLS_MAX_SAT_H_
-#define OPT_SLS_MAX_SAT_H_
-
-#include "maxsmt.h"
-
-namespace opt {
-
-
-    maxsmt_solver_base* mk_sls(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft);
-
-    
-};
-
-#endif
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 992e13fe4..a0dd2aed1 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -21,7 +21,6 @@ Notes:
 #include "maxsmt.h"
 #include "maxres.h"
 #include "wmax.h"
-#include "maxsls.h"
 #include "ast_pp.h"
 #include "uint_set.h"
 #include "opt_context.h"
@@ -163,15 +162,12 @@ namespace opt {
         else if (maxsat_engine == symbol("pd-maxres")) {            
             m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
-        else if (maxsat_engine == symbol("sls")) {                
-            // NB: this is experimental one-round version of SLS
-            m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
-        }        
         else {
             if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
                 warning_msg("solver %s is not recognized, using default 'wmax'", 
                             maxsat_engine.str().c_str());
             }
+            std::cout << "wmax\n";
             m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
         }
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4de602ec4..4eafb93f2 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -561,7 +561,7 @@ namespace opt {
         if (opt_params(m_params).priority() == symbol("pareto")) {
             return;
         }
-        m_params.set_bool("minimize_core_partial", true); // false);
+        m_params.set_bool("minimize_core_partial", true);
         m_params.set_bool("minimize_core", true);
         m_sat_solver = mk_inc_sat_solver(m, m_params);
         expr_ref_vector fmls(m);
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index eb8d61423..a7c9e0011 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -2,7 +2,7 @@ def_module_params('opt',
                   description='optimization parameters',
                   export=True,
                   params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
-	                  ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'sls'"),
+	                  ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('print_model', BOOL, False, 'display model for satisfiable constraints'),
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index 5071563f7..17c5a51bf 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -184,9 +184,10 @@ namespace opt {
             expr_ref tmp(m);
             goal_ref g(alloc(goal, m, true, false));
             for (unsigned i = 0; i < m_solver->get_num_assertions(); ++i) {
-                m_pb2bv(m_solver->get_assertion(i), tmp);
+                m_pb2bv(m_solver->get_assertion(i), tmp);                
                 g->assert_expr(tmp);
             }
+            TRACE("opt", g->display(tout););
             tactic_ref simplify = mk_nnf_tactic(m);
             proof_converter_ref pc;
             expr_dependency_ref core(m);
@@ -198,6 +199,7 @@ namespace opt {
             for (unsigned i = 0; i < r->size(); ++i) {
                 m_bvsls->assert_expr(r->form(i));
             }
+            TRACE("opt", m_bvsls->display(tout););
         }
 
         void pbsls_opt(model_ref& mdl) {
@@ -230,6 +232,7 @@ namespace opt {
             }
             assertions2sls();
             expr_ref objective = soft2bv(m_soft, m_weights);
+            TRACE("opt", tout << objective << "\n";);
             opt_result res(m);
             res.is_sat = l_undef;
             try {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 766ed52be..badb0a67a 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -474,6 +474,9 @@ lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational cons
     for (unsigned i = 0; _weights && i < sz; ++i) {
         weights.push_back(_weights[i].get_double());
     }
+    params_ref p;
+    p.set_bool("minimize_core", false);
+    s.updt_params(p);
     return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double());
 }