diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index d4fef002d..5ff2cc745 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -503,7 +503,8 @@ public:
         TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
         remove_core(corr_set);
         rational w = split_core(corr_set);
-        cs_max_resolve(corr_set, w);        
+        cs_max_resolve(corr_set, w);       
+        IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";);
     }
 
     lbool process_unsat() {
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 73931a3cd..2b8bcb462 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -136,7 +136,6 @@ namespace opt {
         m_wth = s.ensure_wmax_theory();
     }
     maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
-        //m_wth->reset();
     }
     smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
     
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index bb6451c41..3499c51ff 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -40,7 +40,6 @@ namespace opt {
         lbool operator()() {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
-            solver::scoped_push _s1(s());
             lbool is_sat = l_true;
             bool was_sat = false;
             for (unsigned i = 0; i < m_soft.size(); ++i) {
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index 17ec4ff0a..539a3e909 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -171,7 +171,6 @@ void theory_wmaxsat::reset_local() {
     m_vars.reset();
     m_fmls.reset();
     m_rweights.reset();
-    m_costs.reset();
     m_rmin_cost.reset();
     m_rcost.reset();
     m_zweights.reset();