diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 754b2adb2..2c4e22492 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -59,14 +59,15 @@ namespace opt {
                 is_sat = opt::fu_malik_maxsat(*s, fmls_copy);
             }
             else {
-                is_sat = weighted_maxsat(*s, fmls_copy, m_weights);
+                is_sat = weighted_maxsat(get_opt_solver(*s), fmls_copy, m_weights);
             }
             std::cout << "is-sat: " << is_sat << "\n";
             if (is_sat != l_true) {
                 return;
             }
+            std::cout << "Satisfying soft constraints\n";
             for (unsigned i = 0; i < fmls_copy.size(); ++i) {
-                std::cout << "Satisfying soft constraint: " << mk_pp(fmls_copy[i].get(), m) << "\n";
+                std::cout << mk_pp(fmls_copy[i].get(), m) << "\n";
             }            
         }
 
@@ -75,9 +76,7 @@ namespace opt {
             for (unsigned i = 0; i < fmls_copy.size(); ++i) {
                 s->assert_expr(fmls_copy[i].get());
             }
-            // SASSERT(instanceof(*s, opt_solver));
-            // if (!instsanceof ...) { throw ... invalid usage ..} 
-            is_sat = optimize_objectives(dynamic_cast<opt_solver&>(*s), m_objectives, values);
+            is_sat = optimize_objectives(get_opt_solver(*s), m_objectives, values);
             std::cout << "is-sat: " << is_sat << std::endl;
 
             if (is_sat != l_true) {
@@ -108,6 +107,13 @@ namespace opt {
         return true;
     }
 
+    opt_solver& context::get_opt_solver(solver& s) {
+        if (typeid(opt_solver) != typeid(s)) {
+            throw default_exception("BUG: optimization context has not been initialized correctly");
+        }
+        return dynamic_cast<opt_solver&>(s);
+    }
+
     void context::cancel() {
         if (m_solver) {
             m_solver->cancel();
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index a388bc952..866bdf7d3 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -30,6 +30,8 @@ Notes:
 
 namespace opt {
 
+    class opt_solver;
+
     class context {
         ast_manager& m;
         expr_ref_vector  m_hard_constraints;
@@ -70,6 +72,8 @@ namespace opt {
     private:
         bool is_maxsat_problem() const;
 
+        opt_solver& get_opt_solver(solver& s); 
+
     };
 
 }
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index ce07233e3..a9f8da3b0 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -78,6 +78,9 @@ namespace opt {
             toggle_objective(opt_solver& s, bool new_value);
             ~toggle_objective();
         };
+
+        smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat.
+        
     private:
         smt::theory_opt& get_optimizer();
     };
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index a97c237e2..6ec5c4ead 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -20,34 +20,59 @@ Notes:
 #include "smt_theory.h"
 #include "smt_context.h"
 
-namespace opt {
+namespace smt {
 
-    class theory_weighted_maxsat : public smt::theory {
+    class theory_weighted_maxsat : public theory {
+        expr_ref_vector          m_vars;
+        expr_ref_vector          m_fmls;
         vector<rational>         m_weights;    // weights of theory variables.
-        svector<smt::theory_var> m_costs;      // set of asserted theory variables
+        svector<theory_var>      m_costs;      // set of asserted theory variables
         rational                 m_cost;       // current sum of asserted costs
         rational                 m_min_cost;   // current minimal cost assignment.
-        svector<smt::theory_var> m_assignment; // current best assignment.
+        svector<theory_var>      m_assignment; // current best assignment.
     public:
         theory_weighted_maxsat(ast_manager& m):
-            theory(m.get_family_id("weighted_maxsat"))
+            theory(m.get_family_id("weighted_maxsat")),
+            m_vars(m),
+            m_fmls(m)
         {}
 
+        void get_assignment(expr_ref_vector& result) {
+            result.reset();
+            for (unsigned i = 0; i < m_assignment.size(); ++i) {
+                result.push_back(m_fmls[m_assignment[i]].get());
+            }
+        }
+
         void assert_weighted(expr* fml, rational const& w) {
-            smt::bool_var v = smt::null_theory_var;
-            // internalize fml
-            // assert weighted clause. v \/ fml
-            // 
+            context & ctx = get_context();
+            ast_manager& m = get_manager();
+            expr_ref var(m);
+            var = m.mk_fresh_const("w", m.mk_bool_sort());
+            ctx.internalize(fml, false);  // TBD: assume or require simplification?
+            ctx.internalize(var, false);
+            enode* x, *y;
+            x = ctx.get_enode(fml);
+            y = ctx.get_enode(var);
+            theory_var v = mk_var(y);
+            SASSERT(v == m_vars.size());
+            SASSERT(v == m_weights.size());
+            m_vars.push_back(var);
+            m_fmls.push_back(fml);
+            ctx.attach_th_var(y, this, v);
+            literal lx(ctx.get_bool_var(fml));
+            literal ly(ctx.get_bool_var(var));
+            ctx.mk_th_axiom(get_id(), lx, ly);
             m_weights.push_back(w);
             m_min_cost += w;
         }
 
-        virtual void assign_eh(smt::bool_var v, bool is_true) {
-            smt::context& ctx = get_context();
+        virtual void assign_eh(bool_var v, bool is_true) {
             if (is_true) {
+                context& ctx = get_context();
                 rational const& w = m_weights[v];
-                ctx.push_trail(value_trail<smt::context, rational>(m_cost));
-                // TBD: ctx.push_trail(...trail.pop_back(m_costly));
+                ctx.push_trail(value_trail<context, rational>(m_cost));
+                ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
                 m_cost += w;
                 m_costs.push_back(v);
                 if (m_cost > m_min_cost) {
@@ -56,57 +81,92 @@ namespace opt {
             }
         }
 
-        virtual smt::final_check_status final_check_eh() {
+        virtual final_check_status final_check_eh() {
             if (m_cost < m_min_cost) {
                 m_min_cost = m_cost;
                 m_assignment.reset();
                 m_assignment.append(m_costs);
             }
             block();
-            return smt::FC_DONE;
+            return FC_DONE;
         }
 
+        virtual void reset_eh() {
+            theory::reset_eh();
+            m_vars.reset();
+            m_weights.reset();
+            m_costs.reset();
+            m_cost.reset();
+            m_min_cost.reset();
+            m_assignment.reset();
+        }
+
+        virtual theory * mk_fresh(context * new_ctx) { UNREACHABLE(); return 0;} // TBD
+        virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; }
+        virtual bool internalize_term(app * term) { return false; }
+        virtual void new_eq_eh(theory_var v1, theory_var v2) { UNREACHABLE(); }
+        virtual void new_diseq_eh(theory_var v1, theory_var v2) { UNREACHABLE(); }
+
+
     private:
        
         class compare_cost {
             theory_weighted_maxsat& m_th;
         public:
             compare_cost(theory_weighted_maxsat& t):m_th(t) {}
-            bool operator() (smt::theory_var v, smt::theory_var w) const { 
+            bool operator() (theory_var v, theory_var w) const { 
                 return m_th.m_weights[v] < m_th.m_weights[w]; 
             }
         };
 
         void block() {
             ast_manager& m = get_manager();
-            smt::context& ctx = get_context();
-            smt::literal_vector lits;
+            context& ctx = get_context();
+            literal_vector lits;
             compare_cost compare_cost(*this);
-            std::sort(m_costs.begin(), m_costs.end(), compare_cost);
+            svector<theory_var> costs(m_costs);
+            std::sort(costs.begin(), costs.end(), compare_cost);
             rational weight(0);
-            for (unsigned i = 0; i < m_costs.size() && 
-                     weight < m_min_cost; ++i) {
-                weight += m_weights[m_costs[i]];
-                lits.push_back(~smt::literal(m_costs[i]));
+            for (unsigned i = 0; i < costs.size() && weight < m_min_cost; ++i) {
+                weight += m_weights[costs[i]];
+                lits.push_back(~literal(costs[i]));
             }
-            smt::justification * js = 0;
+            justification * js = 0;
             if (m.proofs_enabled()) {
                 js = new (ctx.get_region()) 
-                    smt::theory_lemma_justification(get_id(), ctx, lits.size(), lits.c_ptr());
+                    theory_lemma_justification(get_id(), ctx, lits.size(), lits.c_ptr());
             }
-            ctx.mk_clause(lits.size(), lits.c_ptr(), js, smt::CLS_AUX_LEMMA, 0);
+            ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
         }        
     };
 
+}
+
+namespace opt {
+
+
     /**
        Takes solver with hard constraints added.
        Returns a maximal satisfying subset of weighted soft_constraints
        that are still consistent with the solver state.
     */
     
-    lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
-        NOT_IMPLEMENTED_YET();
-        return l_false;
+    lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights) {
+        ast_manager& m = soft_constraints.get_manager();
+        smt::context& ctx = s.get_context();                        
+        smt::theory_id th_id = m.get_family_id("weighted_maxsat");
+        smt::theory* th = ctx.get_theory(th_id);               
+        if (!th) {
+            th = alloc(smt::theory_weighted_maxsat, m);
+            ctx.register_plugin(th);
+        }
+        smt::theory_weighted_maxsat* wth = dynamic_cast<smt::theory_weighted_maxsat*>(th);
+        for (unsigned i = 0; i < soft_constraints.size(); ++i) {
+            wth->assert_weighted(soft_constraints[i].get(), weights[i]);
+        }
+        lbool result = s.check_sat_core(0,0);
+        wth->get_assignment(soft_constraints);
+        return result;
     }
 };
 
diff --git a/src/opt/weighted_maxsat.h b/src/opt/weighted_maxsat.h
index 542d0bafc..120609a8c 100644
--- a/src/opt/weighted_maxsat.h
+++ b/src/opt/weighted_maxsat.h
@@ -18,7 +18,7 @@ Notes:
 #ifndef _OPT_WEIGHTED_MAX_SAT_H_
 #define _OPT_WEIGHTED_MAX_SAT_H_
 
-#include "solver.h"
+#include "opt_solver.h"
 
 namespace opt {
     /**
@@ -27,7 +27,7 @@ namespace opt {
        that are still consistent with the solver state.
     */
     
-    lbool weighted_maxsat(solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
+    lbool weighted_maxsat(opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights);
 };
 
 #endif