diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp
index cb68b2c0b..89e2e1e51 100644
--- a/src/ast/pb_decl_plugin.cpp
+++ b/src/ast/pb_decl_plugin.cpp
@@ -118,8 +118,8 @@ app * pb_util::mk_at_most_k(unsigned num_args, expr * const * args, unsigned k)
     return m.mk_app(m_fid, OP_AT_MOST_K, 1, &param, num_args, args, m.mk_bool_sort());
 }
 
-bool pb_util::is_at_most_k(app *a) const {
-    return is_app_of(a, m_fid, OP_AT_MOST_K);
+bool pb_util::is_at_most_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_MOST_K);
 }
 
 bool pb_util::is_at_most_k(app *a, rational& k) const {
@@ -138,8 +138,8 @@ app * pb_util::mk_at_least_k(unsigned num_args, expr * const * args, unsigned k)
     return m.mk_app(m_fid, OP_AT_LEAST_K, 1, &param, num_args, args, m.mk_bool_sort());
 }
 
-bool pb_util::is_at_least_k(app *a) const {
-    return is_app_of(a, m_fid, OP_AT_LEAST_K);
+bool pb_util::is_at_least_k(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_AT_LEAST_K);
 }
 
 bool pb_util::is_at_least_k(app *a, rational& k) const {
@@ -152,8 +152,8 @@ bool pb_util::is_at_least_k(app *a, rational& k) const {
     }
 }
 
-rational pb_util::get_k(app *a) const {
-    parameter const& p = a->get_decl()->get_parameter(0);
+rational pb_util::get_k(func_decl *a) const {
+    parameter const& p = a->get_parameter(0);
     if (is_at_most_k(a) || is_at_least_k(a)) {
         return to_rational(p);
     }
@@ -164,8 +164,8 @@ rational pb_util::get_k(app *a) const {
 }
 
 
-bool pb_util::is_le(app *a) const {
-    return is_app_of(a, m_fid, OP_PB_LE);
+bool pb_util::is_le(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_LE);
 }
 
 bool pb_util::is_le(app* a, rational& k) const {
@@ -178,8 +178,8 @@ bool pb_util::is_le(app* a, rational& k) const {
     }
 }
 
-bool pb_util::is_ge(app *a) const {
-    return is_app_of(a, m_fid, OP_PB_GE);
+bool pb_util::is_ge(func_decl *a) const {
+    return is_decl_of(a, m_fid, OP_PB_GE);
 }
 
 bool pb_util::is_ge(app* a, rational& k) const {
@@ -192,13 +192,13 @@ bool pb_util::is_ge(app* a, rational& k) const {
     }
 }
 
-rational pb_util::get_coeff(app* a, unsigned index) {
+rational pb_util::get_coeff(func_decl* a, unsigned index) const {
     if (is_at_most_k(a) || is_at_least_k(a)) {
         return rational::one();
     }
     SASSERT(is_le(a) || is_ge(a));
-    SASSERT(1 + index < a->get_decl()->get_num_parameters());
-    return to_rational(a->get_decl()->get_parameter(index + 1));
+    SASSERT(1 + index < a->get_num_parameters());
+    return to_rational(a->get_parameter(index + 1));
 }
 
 rational pb_util::to_rational(parameter const& p) const {
diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h
index 103f74115..bc186433e 100644
--- a/src/ast/pb_decl_plugin.h
+++ b/src/ast/pb_decl_plugin.h
@@ -82,16 +82,22 @@ public:
     app * mk_at_least_k(unsigned num_args, expr * const * args, unsigned k);
     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);
-    bool is_at_most_k(app *a) const;
+    bool is_at_most_k(func_decl *a) const;
+    bool is_at_most_k(app *a) const { return is_at_most_k(a->get_decl()); }
     bool is_at_most_k(app *a, rational& k) const;
-    bool is_at_least_k(app *a) const;
+    bool is_at_least_k(func_decl *a) const;
+    bool is_at_least_k(app *a) const { return is_at_most_k(a->get_decl()); }
     bool is_at_least_k(app *a, rational& k) const;
-    rational get_k(app *a) const;
-    bool is_le(app *a) const;
+    rational get_k(func_decl *a) const;
+    rational get_k(app *a) const { return get_k(a->get_decl()); }
+    bool is_le(func_decl *a) const;
+    bool is_le(app *a) const { return is_le(a->get_decl()); }
     bool is_le(app* a, rational& k) const;
-    bool is_ge(app* a) const;
+    bool is_ge(func_decl* a) const;
+    bool is_ge(app* a) const { return is_ge(a->get_decl()); }
     bool is_ge(app* a, rational& k) const;
-    rational get_coeff(app* a, unsigned index); 
+    rational get_coeff(app* a, unsigned index) const { return get_coeff(a->get_decl(), index); }
+    rational get_coeff(func_decl* a, unsigned index) const; 
 private:
     rational to_rational(parameter const& p) const;
 };
diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp
new file mode 100644
index 000000000..462944943
--- /dev/null
+++ b/src/ast/rewriter/pb_rewriter.cpp
@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+
+#include "pb_rewriter.h"
+
+br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    ast_manager& m = result.get_manager();
+    rational sum(0), maxsum(0);
+    for (unsigned i = 0; i < num_args; ++i) {
+        if (m.is_true(args[i])) {
+            sum += m_util.get_coeff(f, i);
+            maxsum += m_util.get_coeff(f, i);
+        }
+        else if (!m.is_false(args[i])) {
+            maxsum += m_util.get_coeff(f, i);            
+        }
+    }
+    rational k = m_util.get_k(f);
+    
+    switch(f->get_decl_kind()) {
+    case OP_AT_MOST_K:
+    case OP_PB_LE:
+        if (sum > k) {
+            result = m.mk_false();
+            return BR_DONE;
+        }
+        if (maxsum <= k) {
+            result = m.mk_true();
+            return BR_DONE;
+        }
+        return BR_FAILED;
+    case OP_AT_LEAST_K:
+    case OP_PB_GE:
+        if (sum >= k) {
+            result = m.mk_true();
+            return BR_DONE;
+        }
+        if (maxsum < k) {
+            result = m.mk_false();
+            return BR_DONE;
+        }
+        return BR_FAILED;
+    default:
+        UNREACHABLE();
+        return BR_FAILED;
+    }    
+}
+
+
diff --git a/src/ast/rewriter/pb_rewriter.h b/src/ast/rewriter/pb_rewriter.h
new file mode 100644
index 000000000..da020cb7c
--- /dev/null
+++ b/src/ast/rewriter/pb_rewriter.h
@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    pb_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for PB constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-14-12
+
+Notes:
+
+--*/
+#ifndef _PB_REWRITER_H_
+#define _PB_REWRITER_H_
+
+#include"pb_decl_plugin.h"
+#include"rewriter_types.h"
+#include"params.h"
+
+/**
+   \brief Cheap rewrite rules for PB constraints
+*/
+class pb_rewriter {
+    pb_util       m_util;
+public:    
+    pb_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        m_util(m) {
+    }
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    void updt_params(params_ref const & p) {}
+    static void get_param_descrs(param_descrs & r) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+};
+
+#endif
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 5d19c53e3..83f88739e 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"array_rewriter.h"
 #include"float_rewriter.h"
 #include"dl_rewriter.h"
+#include"pb_rewriter.h"
 #include"rewriter_def.h"
 #include"expr_substitution.h"
 #include"ast_smt2_pp.h"
@@ -41,6 +42,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     datatype_rewriter   m_dt_rw;
     float_rewriter      m_f_rw;
     dl_rewriter         m_dl_rw;
+    pb_rewriter         m_pb_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
     unsigned long long  m_max_memory; // in bytes
@@ -195,6 +197,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return m_f_rw.mk_app_core(f, num, args, result);
         if (fid == m_dl_rw.get_fid())
             return m_dl_rw.mk_app_core(f, num, args, result);
+        if (fid == m_pb_rw.get_fid())
+            return m_pb_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
     }
 
@@ -644,6 +648,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_dt_rw(m),
         m_f_rw(m, p),
         m_dl_rw(m),
+        m_pb_rw(m),
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 41bca940d..9bb17f730 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -23,6 +23,7 @@ Revision History:
 #include"bool_rewriter.h"
 #include"arith_rewriter.h"
 #include"bv_rewriter.h"
+#include"pb_rewriter.h"
 #include"datatype_rewriter.h"
 #include"array_rewriter.h"
 #include"float_rewriter.h"
@@ -36,6 +37,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     bv_rewriter                     m_bv_rw;
     array_rewriter                  m_ar_rw;
     datatype_rewriter               m_dt_rw;
+    pb_rewriter                     m_pb_rw;
     float_rewriter                  m_f_rw;
     unsigned long long              m_max_memory;
     unsigned                        m_max_steps;
@@ -52,6 +54,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         // See comment above. We want to allow customers to set :sort-store
         m_ar_rw(m, p),
         m_dt_rw(m),
+        m_pb_rw(m),
         m_f_rw(m) {
         m_b_rw.set_flat(false);
         m_a_rw.set_flat(false);
@@ -153,6 +156,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
             return m_ar_rw.mk_app_core(f, num, args, result);
         if (fid == m_dt_rw.get_fid())
             return m_dt_rw.mk_app_core(f, num, args, result);
+        if (fid == m_pb_rw.get_fid())
+            return m_pb_rw.mk_app_core(f, num, args, result);
         if (fid == m_f_rw.get_fid())
             return m_f_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index db6a017b2..3769bdd73 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -322,6 +322,7 @@ namespace opt {
                 for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
                     expr_ref val(m);
                     VERIFY(m_model->eval(m_orig_soft[i].get(), val));
+                    TRACE("opt", tout << val << "\n";);
                     m_assignment.push_back(m.is_true(val));                        
                 }
                 TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 0d459c44d..3b0f684e8 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -112,25 +112,18 @@ namespace opt {
         for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
             expr_ref tmp(m);
             tmp = m_soft_constraints[i].get();
-            if (get_assignment(i)) {
-                m_s->assert_expr(tmp);
-            }
-            else {
+            if (!get_assignment(i)) {
                 tmp = m.mk_not(tmp);
-                m_s->assert_expr(tmp);
             }
+            TRACE("opt", tout << "asserting: " << tmp << "\n";);
+            m_s->assert_expr(tmp);            
         }
     }
 
     void maxsmt::display_answer(std::ostream& out) const {
         for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
-            out << mk_pp(m_soft_constraints[i], m);
-            if (get_assignment(i)) {
-                out << " |-> true\n";
-            }
-            else {
-                out << " |-> false\n";
-            }
+            out << mk_pp(m_soft_constraints[i], m)
+                << (get_assignment(i)?" |-> true\n":" |-> false\n");
         }
     }
     
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 48274c502..26ce2152b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -121,7 +121,7 @@ namespace opt {
 
     lbool context::execute_min_max(unsigned index, bool committed) {
         lbool result = m_optsmt.lex(index);
-        if (committed) m_optsmt.commit_assignment(index);
+        if (result == l_true && committed) m_optsmt.commit_assignment(index);
         if (result == l_true) m_optsmt.get_model(m_model);
         return result;
     }
@@ -129,7 +129,7 @@ namespace opt {
     lbool context::execute_maxsat(symbol const& id, bool committed) {
         maxsmt& ms = *m_maxsmts.find(id);
         lbool result = ms(get_solver());
-        if (committed) ms.commit_assignment();
+        if (result == l_true && committed) ms.commit_assignment();
         if (result == l_true) ms.get_model(m_model);
         return result;
     }
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 99d9287a5..45eab4d76 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -48,6 +48,7 @@ namespace smt {
         */
         void get_assignment(svector<bool>& result) {
             result.reset();
+
             std::sort(m_cost_save.begin(), m_cost_save.end());
             for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
                 if (j < m_cost_save.size() && m_cost_save[j] == i) {
@@ -58,43 +59,58 @@ namespace smt {
                     result.push_back(true);
                 }
             }
+            TRACE("opt",
+                  tout << "cost save: ";
+                  for (unsigned i = 0; i < m_cost_save.size(); ++i) {
+                      tout << m_cost_save[i] << " ";
+                  }
+                  tout << "\nvars: ";
+                  for (unsigned i = 0; i < m_vars.size(); ++i) {
+                      tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
+                  }
+                  tout << "\nassignment";
+                  for (unsigned i = 0; i < result.size(); ++i) {
+                      tout << result[i] << " ";
+                  }
+                  tout << "\n";);                  
+
         }
 
         virtual void init_search_eh() {
             context & ctx = get_context();
             ast_manager& m = get_manager();
-            m_var2bool.reset();
-            for (unsigned i = 0; i < m_vars.size(); ++i) {
+            bool initialized = !m_var2bool.empty();
+            
+            for (unsigned i = 0; !initialized && i < m_vars.size(); ++i) {
                 app* var = m_vars[i].get();  
                 bool_var bv;
-                enode* x;
-                if (!ctx.e_internalized(var)) {
-                    x = ctx.mk_enode(var, false, true, true);
-                }
-                else {
-                    x = ctx.get_enode(var);
-                }
+                theory_var v;
+                SASSERT(!ctx.e_internalized(var));
+                enode* x = ctx.mk_enode(var, false, true, true);
                 if (ctx.b_internalized(var)) {
                     bv = ctx.get_bool_var(var);
                 }
                 else {
                     bv = ctx.mk_bool_var(var);
                 }
-                ctx.set_var_theory(bv, get_id());
+                ctx.set_var_theory(bv, get_id());                    
                 ctx.set_enode_flag(bv, true);
-                theory_var v = mk_var(x);
+                v = mk_var(x);
                 ctx.attach_th_var(x, this, v);
                 m_bool2var.insert(bv, v);
                 SASSERT(v == m_var2bool.size());
                 m_var2bool.push_back(bv);
                 SASSERT(ctx.bool_var2enode(bv));
-
+            }
+            for (unsigned i = 0; i < m_vars.size(); ++i) {
+                app* var = m_vars[i].get();  
+                bool_var bv = ctx.get_bool_var(var);
                 lbool asgn = ctx.get_assignment(bv);
                 if (asgn == l_true) {
                     assign_eh(bv, true);
                 }
-
             }
+
             if (m_min_cost_atom) {
                 app* var = m_min_cost_atom;
                 if (!ctx.e_internalized(var)) {
@@ -157,10 +173,7 @@ namespace smt {
         }
 
         virtual final_check_status final_check_eh() {
-            if (block(true)) {
-                return FC_DONE;
-            }
-            return FC_CONTINUE;
+            return FC_DONE;
         }
 
         virtual bool use_diseqs() const { 
@@ -171,7 +184,7 @@ namespace smt {
             return false;
         }
 
-        void reset() {
+        void reset() {            
             reset_eh();
         }
 
@@ -195,17 +208,9 @@ namespace smt {
         virtual void new_eq_eh(theory_var v1, theory_var v2) { }
         virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
 
-
-    private:
-       
-        class compare_cost {
-            theory_weighted_maxsat& m_th;
-        public:
-            compare_cost(theory_weighted_maxsat& t):m_th(t) {}
-            bool operator() (theory_var v, theory_var w) const { 
-                return m_th.m_weights[v] > m_th.m_weights[w]; 
-            }
-        };
+        bool is_optimal() const {
+            return m_cost < m_min_cost;
+        }
 
         bool block(bool is_final) {
             if (m_vars.empty()) {
@@ -225,18 +230,27 @@ namespace smt {
             if (m_min_cost_atom) {
                 lits.push_back(~literal(m_min_cost_bv));
             }
-            IF_VERBOSE(2,
-                       verbose_stream() << "block: ";
-                       for (unsigned i = 0; i < lits.size(); ++i) {
-                           expr_ref tmp(m);
-                           ctx.literal2expr(lits[i], tmp);
-                           verbose_stream() << tmp << " ";
-                       }
-                       verbose_stream() << "\n";
-                       );
+            TRACE("opt",
+                  tout << "block" << (is_final?" final: ":": ");;
+                  for (unsigned i = 0; i < lits.size(); ++i) {
+                      expr_ref tmp(m);
+                      ctx.literal2expr(lits[i], tmp);
+                      tout << tmp << " ";
+                  }
+                  tout << "\n";
+                  if (is_final && is_optimal()) {
+                      tout << "costs: ";
+                      for (unsigned i = 0; i < m_costs.size(); ++i) {
+                          tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
+                      }
+                      tout << "\n";
+                      ctx.display(tout);
+                      
+                  }
+                  );
 
             ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-            if (is_final && m_cost < m_min_cost) {
+            if (is_final && is_optimal()) {
                 m_min_cost = weight;
                 m_cost_save.reset();
                 m_cost_save.append(m_costs);
@@ -244,6 +258,19 @@ namespace smt {
             return false;
         }                
 
+
+    private:
+       
+        class compare_cost {
+            theory_weighted_maxsat& m_th;
+        public:
+            compare_cost(theory_weighted_maxsat& t):m_th(t) {}
+            bool operator() (theory_var v, theory_var w) const { 
+                return m_th.m_weights[v] > m_th.m_weights[w]; 
+            }
+        };
+
+
     };
 
 }
@@ -329,26 +356,36 @@ namespace opt {
         lbool operator()() {
             TRACE("opt", tout << "weighted maxsat\n";);
             smt::theory_weighted_maxsat& wth = ensure_theory();
-            lbool result;
+            lbool is_sat = l_true;
             {
                 solver::scoped_push _s(s);
                 for (unsigned i = 0; i < m_soft.size(); ++i) {
                     wth.assert_weighted(m_soft[i].get(), m_weights[i]);
                 }
-                result = s.check_sat_core(0,0);
-                SASSERT(result != l_true);
-                wth.get_assignment(m_assignment);
-                if (result == l_false) {
-                    result = l_true;
+                while (l_true == is_sat) {
+                    is_sat = s.check_sat_core(0,0);
+                    if (is_sat == l_true) {
+                        if (wth.is_optimal()) {
+                            s.get_model(m_model);
+                        }
+                        wth.block(true);                        
+                        if (s.get_context().inconsistent()) {
+                            is_sat = l_false;
+                        }
+                    }
+                }
+                if (is_sat == l_false) {
+                    wth.get_assignment(m_assignment);
+                    is_sat = l_true;
                 }
             }
             m_upper = wth.get_min_cost();
-            if (result == l_true) {
+            if (is_sat == l_true) {
                 m_lower = m_upper;
             }
             TRACE("opt", tout << "min cost: " << m_upper << "\n";);
             wth.reset();
-            return result;            
+            return is_sat;            
         }        
 
         rational get_lower() const {
@@ -360,10 +397,7 @@ namespace opt {
         }
 
         void get_model(model_ref& mdl) {
-            lbool is_sat = s.check_sat_core(0,0);
-            if (is_sat == l_true) {
-                s.get_model(mdl);
-            }
+            mdl = m_model.get();
         }
 
     };
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 33cc4105e..07e88a3a0 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -23,6 +23,7 @@ Notes:
 #include "ast_pp.h"
 #include "sorting_network.h"
 #include "uint_set.h"
+#include "smt_model_generator.h"
 
 namespace smt {
 
@@ -1458,6 +1459,89 @@ namespace smt {
         return out;
     }
 
+    class theory_pb::pb_model_value_proc : public model_value_proc {
+        app*              m_app;
+        svector<model_value_dependency> m_dependencies;
+    public:
+
+        pb_model_value_proc(app* a): 
+            m_app(a) {}
+
+        void add(enode* n) { 
+            m_dependencies.push_back(model_value_dependency(n)); 
+        }
+
+        virtual void get_dependencies(buffer<model_value_dependency> & result) {
+            result.append(m_dependencies.size(), m_dependencies.c_ptr());
+        }
+
+        virtual app * mk_value(model_generator & mg, ptr_vector<expr> & values) {
+            ast_manager& m = mg.get_manager();
+            SASSERT(values.size() == m_dependencies.size());
+            SASSERT(values.size() == m_app->get_num_args());
+            pb_util u(m);
+            rational sum(0);
+            for (unsigned i = 0; i < m_app->get_num_args(); ++i) {
+                if (!m.is_true(values[i]) && !m.is_false(values[i])) {
+                    return m_app;
+                }
+                if (m.is_true(values[i])) {
+                    sum += u.get_coeff(m_app, i);
+                }
+            }
+            rational k = u.get_k(m_app);
+            switch(m_app->get_decl_kind()) {
+            case OP_AT_MOST_K:
+                return (sum <= k)?m.mk_true():m.mk_false();
+            case OP_AT_LEAST_K:
+                return (sum >= k)?m.mk_true():m.mk_false();
+            case OP_PB_LE:
+                return (sum <= k)?m.mk_true():m.mk_false();
+            case OP_PB_GE:
+                return (sum >= k)?m.mk_true():m.mk_false();
+            default:
+                UNREACHABLE();
+                return 0;
+            }
+            return 0;
+        }
+    };
+
+    class pb_factory : public value_factory {
+    public:
+        pb_factory(ast_manager& m, family_id fid):
+            value_factory(m, fid) {}
+        
+        virtual expr * get_some_value(sort * s) {
+            return m_manager.mk_true();
+        }        
+        virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+            v1 = m_manager.mk_true();
+            v2 = m_manager.mk_false();
+            return true;
+        }        
+        virtual expr * get_fresh_value(sort * s) {
+            return 0;
+        }
+        virtual void register_value(expr * n) { }
+    };
+
+    void theory_pb::init_model(model_generator & m) {
+        std::cout << "init model\n";
+        m.register_factory(alloc(pb_factory, get_manager(), get_id()));
+    }
+
+    model_value_proc * theory_pb::mk_value(enode * n, model_generator & mg) {
+        std::cout << "mk-value " << mk_pp(n->get_owner(), get_manager()) << "\n";
+        context& ctx = get_context();
+        app* a = n->get_owner();
+        pb_model_value_proc* p = alloc(pb_model_value_proc, a);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            p->add(ctx.get_enode(a->get_arg(i)));
+        }
+        return p;
+    }
+
     void theory_pb::display(std::ostream& out) const {
         u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
         for (; it != end; ++it) {
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 34cd479a1..c5387471d 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -29,6 +29,7 @@ namespace smt {
 
         struct sort_expr;
         class  pb_justification;
+        class pb_model_value_proc;
         typedef rational numeral;
         typedef vector<std::pair<literal, numeral> > arg_t;
 
@@ -181,6 +182,7 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual void restart_eh();
         virtual void collect_statistics(::statistics & st) const;
-        
+        virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+        virtual void init_model(model_generator & m);        
     };
 };