diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 97b6a5293..f93291599 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -55,15 +55,18 @@ namespace opt {
 
     void maxsmt_solver_base::commit_assignment() {
         expr_ref tmp(m);
-        rational k(0);
+        rational k(0), cost(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             if (get_assignment(i)) {
                 k += m_weights[i];
             }
+            else {
+                cost += m_weights[i];
+            }
         }       
         pb_util pb(m);
         tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
-        TRACE("opt", tout << tmp << "\n";);
+        TRACE("opt", tout << "cost: " << cost << "\n" << tmp << "\n";);
         s().assert_expr(tmp);
     }
 
@@ -140,7 +143,9 @@ namespace opt {
         m_wth = s.ensure_wmax_theory();
     }
     maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
-        //m_wth->reset_local();
+        if (m_wth) {
+            m_wth->reset_local();
+        }
     }
     smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
 
@@ -226,7 +231,9 @@ namespace opt {
         m_msolver = 0;
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
-        TRACE("opt", tout << "maxsmt\n";);
+        TRACE("opt", tout << "maxsmt\n";
+              s().display(tout); tout << "\n";
+              );
         if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
             m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 42129be70..351141a3f 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -327,12 +327,7 @@ namespace opt {
         SASSERT(idx < get_num_assertions());
         return m_context.get_formulas()[idx];
     }
-    
-    std::ostream& opt_solver::display(std::ostream & out) const {
-        m_context.display(out);
-        return out;
-    }
-    
+        
     smt::theory_var opt_solver::add_objective(app* term) {
         smt::theory_var v = get_optimizer().add_objective(term);
         m_objective_vars.push_back(v);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index cdaad3cf2..27168e2ca 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -104,7 +104,6 @@ namespace opt {
         virtual void set_progress_callback(progress_callback * callback);
         virtual unsigned get_num_assertions() const;
         virtual expr * get_assertion(unsigned idx) const;
-        virtual std::ostream& display(std::ostream & out) const;
         virtual ast_manager& get_manager() const { return m; } 
         virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
         virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 690e2000b..9708bdc8f 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -64,6 +64,7 @@ namespace opt {
             bool was_sat = false;
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
+
             obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
             for (; it != end; ++it) {
                 expr* c = assert_weighted(wth(), it->m_key, it->m_value);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ea97d1a64..c7aecca88 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1795,6 +1795,7 @@ namespace smt {
 
     void context::set_conflict(b_justification js, literal not_l) {
         if (!inconsistent()) {
+            TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
             m_conflict = js;
             m_not_l    = not_l;
         }