diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index b52c7d9b9..b6950f674 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -544,18 +544,11 @@ public:
             return l_true;
         }
         m_mus.reset();
-        for (unsigned i = 0; i < core.size(); ++i) {
-            VERIFY(i == m_mus.add_soft(core[i]));
-        }
-        unsigned_vector mus_idx;
-        lbool is_sat = m_mus.get_mus(mus_idx);
+        m_mus.add_soft(core.size(), core.c_ptr());
+        lbool is_sat = m_mus.get_mus(m_new_core);
         if (is_sat != l_true) {
             return is_sat;
         }
-        m_new_core.reset();
-        for (unsigned i = 0; i < mus_idx.size(); ++i) {
-            m_new_core.push_back(core[mus_idx[i]]);
-        }
         core.reset();
         core.append(m_new_core);
         return l_true;
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 74b6769ae..02c6d26cd 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -811,14 +811,10 @@ namespace qe {
             }
             TRACE("qe", tout << core1.size() << " " << core2.size() << "\n";);
             if (core1.size() > 8) {
-                unsigned_vector core_idxs;
-                if (l_true != mus.get_mus(core_idxs)) {
+                if (l_true != mus.get_mus(core2)) {
                     return false;
                 }
-                TRACE("qe", tout << core1.size() << " -> " << core_idxs.size() << "\n";);
-                for (unsigned i = 0; i < core_idxs.size(); ++i) {
-                    core2.push_back(core1[core_idxs[i]].get());
-                }
+                TRACE("qe", tout << core1.size() << " -> " << core2.size() << "\n";);
                 core.reset();
                 core.append(core2);
             }
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index a9f6ccc18..153d948f5 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -61,5 +61,6 @@ def_module_params(module_name='smt',
                           ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
-                          ('core.validate', BOOL, False, 'validate unsat core produced by SMT context')
+                          ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context')
                           ))
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 59c08006b..6ae7f107c 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -20,19 +20,25 @@ Notes:
 #include"smt_kernel.h"
 #include"reg_decl_plugins.h"
 #include"smt_params.h"
+#include"smt_params_helper.hpp"
+#include"mus.h"
 
 namespace smt {
 
     class solver : public solver_na2as {
-        smt_params          m_params;
+        smt_params          m_smt_params;
+        params_ref          m_params;
         smt::kernel         m_context;
         progress_callback * m_callback;
         symbol              m_logic;
+        bool                m_minimizing_core;
     public:
         solver(ast_manager & m, params_ref const & p, symbol const & l):
             solver_na2as(m),
+            m_smt_params(p),
             m_params(p),
-            m_context(m, m_params) {
+            m_context(m, m_smt_params),
+            m_minimizing_core(false) {
             m_logic = l;
             if (m_logic != symbol::null)
                 m_context.set_logic(m_logic);
@@ -48,7 +54,8 @@ namespace smt {
         }
 
         virtual void updt_params(params_ref const & p) {
-            m_params.updt_params(p);
+            m_smt_params.updt_params(p);
+            m_params.copy(p);
             m_context.updt_params(p);
         }
 
@@ -77,10 +84,37 @@ namespace smt {
             return m_context.check(num_assumptions, assumptions);
         }
 
+        struct scoped_minimize_core {
+            solver& s;
+            expr_ref_vector m_assumptions;
+            scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) {
+                s.m_minimizing_core = true;
+                s.m_assumptions.reset();
+            }
+
+            ~scoped_minimize_core() {
+                s.m_minimizing_core = false;
+                s.m_assumptions.append(m_assumptions);
+            }
+        };
+
         virtual void get_unsat_core(ptr_vector<expr> & r) {
             unsigned sz = m_context.get_unsat_core_size();
-            for (unsigned i = 0; i < sz; i++)
+            for (unsigned i = 0; i < sz; i++) {
                 r.push_back(m_context.get_unsat_core_expr(i));
+            }
+
+            if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) {
+                return;
+            }
+            scoped_minimize_core scm(*this);
+            mus mus(*this);
+            mus.add_soft(r.size(), r.c_ptr());
+            ptr_vector<expr> r2;
+            if (l_true == mus.get_mus(r2)) {
+                r.reset();
+                r.append(r2);
+            }
         }
 
         virtual void get_model(model_ref & m) {
diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp
index 4960a3d2a..adfe42192 100644
--- a/src/solver/mus.cpp
+++ b/src/solver/mus.cpp
@@ -22,10 +22,13 @@ Notes:
 #include "mus.h"
 #include "ast_pp.h"
 #include "ast_util.h"
-#include "uint_set.h"
+#include "model_evaluator.h"
 
 
 struct mus::imp {
+
+    typedef obj_hashtable<expr> expr_set;
+
     solver&                  m_solver;
     ast_manager&             m;
     expr_ref_vector          m_lit2expr;
@@ -56,7 +59,7 @@ struct mus::imp {
         unsigned idx = m_lit2expr.size();
         m_expr2lit.insert(lit, idx);
         m_lit2expr.push_back(lit);
-        TRACE("opt", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";);
+        TRACE("mus", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";);
         return idx;
     }
 
@@ -64,66 +67,61 @@ struct mus::imp {
         SASSERT(is_literal(lit));
         m_assumptions.push_back(lit);
     }
-    
-    lbool get_mus(unsigned_vector& mus) {
-        // SASSERT: mus does not have duplicates.
+
+    lbool get_mus(expr_ref_vector& mus) {
         m_model.reset();
-        unsigned_vector core;
-        for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
-            core.push_back(i);
-        }
-        if (core.size() == 1) {
-            mus.push_back(core.back());
+        mus.reset();
+        if (m_lit2expr.size() == 1) {
+            mus.push_back(m_lit2expr.back());
             return l_true;
         }
+        return get_mus1(mus);
+    }
 
+    lbool get_mus(ptr_vector<expr>& mus) {
         mus.reset();
-        if (false && core.size() > 64) {
-            return qx(mus);
-        }
+        expr_ref_vector result(m);
+        lbool r = get_mus(result);
+        mus.append(result.size(), result.c_ptr());
+        return r;
+    }    
 
-        expr_ref_vector assumptions(m);
+    lbool get_mus1(expr_ref_vector& mus) {
+        ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
         ptr_vector<expr> core_exprs;
-        while (!core.empty()) { 
-            IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
-            unsigned lit_id = core.back();
-            TRACE("opt", 
-                  display_vec(tout << "core:  ", core);
-                  display_vec(tout << "mus:   ", mus);
-                  );
-            core.pop_back();
-            expr* lit = m_lit2expr[lit_id].get();
-            expr_ref not_lit(m);
-            not_lit = mk_not(m, lit);
+        while (!unknown.empty()) { 
+            IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
+            TRACE("mus", display_vec(tout << "core:  ", unknown); display_vec(tout << "mus:   ", mus););
+            expr* lit = unknown.back();
+            unknown.pop_back();
+            expr_ref not_lit(mk_not(m, lit), m);
             lbool is_sat = l_undef;
             {
-                scoped_append _sa1(*this, assumptions, core);
-                scoped_append _sa2(*this, assumptions, m_assumptions);
-                assumptions.push_back(not_lit);
-                is_sat = m_solver.check_sat(assumptions);
+                scoped_append _sa1(*this, mus, unknown);
+                scoped_append _sa2(*this, mus, m_assumptions);
+                mus.push_back(not_lit);
+                is_sat = m_solver.check_sat(mus);
             }
             switch (is_sat) {
             case l_undef: 
                 return is_sat;
             case l_true:
-                assumptions.push_back(lit);
-                mus.push_back(lit_id);
+                mus.push_back(lit);
                 update_model();
                 break;
             default:
                 core_exprs.reset();
                 m_solver.get_unsat_core(core_exprs);
                 if (!core_exprs.contains(not_lit)) {
-                    // core := core_exprs \ mus
-                    core.reset();
+                    // unknown := core_exprs \ mus
+                    unknown.reset();
                     for (unsigned i = 0; i < core_exprs.size(); ++i) {
-                        lit = core_exprs[i];
-                        if (m_expr2lit.find(lit, lit_id) && !mus.contains(lit_id)) {
-                            core.push_back(lit_id);
+                        if (!mus.contains(core_exprs[i])) {
+                            unknown.push_back(core_exprs[i]);
                         }
                     }
-                    TRACE("opt", display_vec(tout << "core exprs:", core_exprs);
-                        display_vec(tout << "core:", core);
+                    TRACE("mus", display_vec(tout << "core exprs:", core_exprs);
+                        display_vec(tout << "core:", unknown);
                         display_vec(tout << "mus:", mus);
                     );
 
@@ -131,36 +129,146 @@ struct mus::imp {
                 break;
             }
         }
-#if 0
-        DEBUG_CODE(
-            assumptions.reset();
-            for (unsigned i = 0; i < mus.size(); ++i) {
-                assumptions.push_back(m_lit2expr[mus[i]].get());
-            }
-            lbool is_sat = m_solver.check_sat(assumptions.size(), assumptions.c_ptr());
-            SASSERT(is_sat == l_false);
-                   );
-#endif
+        // SASSERT(is_core(mus));
         return l_true;
     }
 
+    // use correction sets
+    lbool get_mus2(expr_ref_vector& mus) {
+        expr* lit = 0;
+        lbool is_sat;
+        ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
+        while (!unknown.empty()) { 
+            IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
+            {
+                scoped_append _sa1(*this, mus, m_assumptions);
+                is_sat = get_next_mcs(mus, unknown, lit);
+            }
+            if (l_false == is_sat) {
+                mus.push_back(lit);
+            }
+            else {
+                return is_sat;
+            }
+        }        
+        
+        //SASSERT(is_core(mus));
+        return l_true;
+    }
+
+    // find the next literal to be a member of a core.
+    lbool get_next_mcs(expr_ref_vector& mus, ptr_vector<expr>& unknown, expr*& core_literal) {
+        ptr_vector<expr> mss;
+        expr_ref_vector  nmcs(m);
+        expr_set core, min_core, nmcs_set;
+        bool min_core_valid = false;
+        expr* min_lit = 0;
+        while (!unknown.empty()) {
+            expr* lit = unknown.back();
+            unknown.pop_back();
+            model_ref mdl;
+            scoped_append assume_mss(*this,  mus, mss);      // current satisfied literals
+            scoped_append assume_nmcs(*this, mus, nmcs);     // current non-satisfied literals
+            scoped_append assume_lit(*this,  mus, lit);      // current unknown literal
+            switch (m_solver.check_sat(mus)) {
+            case l_true: {
+                TRACE("mus", tout << "literal can be satisfied: " << mk_pp(lit, m) << "\n";);
+                mss.push_back(lit);
+                m_solver.get_model(mdl);
+                model_evaluator eval(*mdl.get());
+                for (unsigned i = 0; i < unknown.size(); ) {
+                    expr_ref tmp(m);
+                    eval(unknown[i], tmp);
+                    if (m.is_true(tmp)) {
+                        mss.push_back(unknown[i]);
+                        unknown[i] = unknown.back();
+                        unknown.pop_back();
+                    }
+                    else {
+                        ++i;
+                    }
+                }
+                break;
+            }
+            case l_false:
+                TRACE("mus", tout << "literal is in a core: " << mk_pp(lit, m) << "\n";);
+                nmcs.push_back(mk_not(m, lit));
+                nmcs_set.insert(nmcs.back());
+                get_core(core);
+                if (!core.contains(lit)) {
+                    // The current mus is already a core.
+                    unknown.reset();
+                    return l_true;
+                }
+                if (have_intersection(nmcs_set, core)) {
+                    // can't use this core directly. Hypothetically, we 
+                    // could try to combine min_core with core and
+                    // see if the combination produces a better minimal core.
+                    SASSERT(min_core_valid);
+                    break;
+                }
+                if (!min_core_valid || core.size() < min_core.size()) {
+                    // The current core is smallest so far, so we get fewer unknowns from it.
+                    min_core = core;
+                    min_core_valid = true;
+                    min_lit = lit;
+                }
+                break;
+            case l_undef:
+                return l_undef;
+            }
+        }
+        SASSERT(min_core_valid);
+        if (!min_core_valid) {
+            // all unknown soft constraints were satisfiable
+            return l_true;
+        }
+
+        expr_set mss_set;
+        for (unsigned i = 0; i < mss.size(); ++i) {
+            mss_set.insert(mss[i]);
+        }
+        expr_set::iterator it = min_core.begin(), end = min_core.end();
+        for (; it != end; ++it) {
+            if (mss_set.contains(*it) && min_lit != *it) {
+                unknown.push_back(*it);
+            }
+        }
+        core_literal = min_lit;
+        
+        return l_false;
+    }
+
+    bool have_intersection(expr_set const& A, expr_set const& B) {
+        if (A.size() < B.size()) {
+            expr_set::iterator it = A.begin(), end = A.end();
+            for (; it != end; ++it) {
+                if (B.contains(*it)) return true;
+            }
+        }
+        else {
+            expr_set::iterator it = B.begin(), end = B.end();
+            for (; it != end; ++it) {
+                if (A.contains(*it)) return true;
+            }
+        }
+        return false;
+    }
+
+    bool is_core(expr_ref_vector const& mus) {
+        return l_false == m_solver.check_sat(mus); 
+    }
+
     class scoped_append {
         expr_ref_vector& m_fmls;
         unsigned         m_size;
     public:
-        scoped_append(imp& imp, expr_ref_vector& fmls1, unsigned_vector const& fmls2):
+        scoped_append(imp& imp, expr_ref_vector& fmls1, expr_set const& fmls2):
             m_fmls(fmls1),
             m_size(fmls1.size()) {
-            for (unsigned i = 0; i < fmls2.size(); ++i) {
-                fmls1.push_back(imp.m_lit2expr[fmls2[i]].get());
-            }            
-        }
-        scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2):
-            m_fmls(fmls1),
-            m_size(fmls1.size()) {
-            uint_set::iterator it = fmls2.begin(), end = fmls2.end();
+            expr_set::iterator it = fmls2.begin(), end = fmls2.end();
             for (; it != end; ++it) {
-                fmls1.push_back(imp.m_lit2expr[*it].get());
+                fmls1.push_back(*it);
             }            
         }
         scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2):
@@ -168,17 +276,21 @@ struct mus::imp {
             m_size(fmls1.size()) {
             fmls1.append(fmls2);
         }
+        scoped_append(imp& imp, expr_ref_vector& fmls1, ptr_vector<expr> const& fmls2):
+            m_fmls(fmls1),
+            m_size(fmls1.size()) {
+            fmls1.append(fmls2.size(), fmls2.c_ptr());
+        }
+        scoped_append(imp& imp, expr_ref_vector& fmls1, expr* fml):
+            m_fmls(fmls1),
+            m_size(fmls1.size()) {
+            fmls1.push_back(fml);
+        }
         ~scoped_append() {
             m_fmls.shrink(m_size);
         }
     };
 
-    void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) {
-        for (unsigned i = 0; i < core.size(); ++i) {
-            assumptions.push_back(m_lit2expr[core[i]].get());
-        }
-    }
-
     template<class T>
     void display_vec(std::ostream& out, T const& v) const {
         for (unsigned i = 0; i < v.size(); ++i) {
@@ -234,14 +346,14 @@ struct mus::imp {
     }
 
 
-    lbool qx(unsigned_vector& mus) {
-        uint_set core, support;
+    lbool qx(expr_ref_vector& mus) {
+        expr_set core, support;
         for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
-            core.insert(i);
+            core.insert(m_lit2expr[i].get());
         }
         lbool is_sat = qx(core, support, false);
         if (is_sat == l_true) {
-            uint_set::iterator it = core.begin(), end = core.end();
+            expr_set::iterator it = core.begin(), end = core.end();
             mus.reset();
             for (; it != end; ++it) {
                 mus.push_back(*it);
@@ -250,7 +362,7 @@ struct mus::imp {
         return is_sat;
     }
 
-    lbool qx(uint_set& assignment, uint_set& support, bool has_support) {
+    lbool qx(expr_set& assignment, expr_set& support, bool has_support) {
         lbool is_sat = l_true;
 #if 0
         if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
@@ -265,7 +377,7 @@ struct mus::imp {
             is_sat = m_solver.check_sat(asms);
             switch (is_sat) {
             case l_false: {
-                uint_set core; 
+                expr_set core; 
                 get_core(core);
                 support &= core;
                 assignment.reset();
@@ -280,10 +392,10 @@ struct mus::imp {
                 break;
             }
         }
-        if (assignment.num_elems() == 1) {
+        if (assignment.size() == 1) {
             return l_true;
         }
-        uint_set assign2;
+        expr_set assign2;
         split(assignment, assign2);
         support |= assignment;
         is_sat = qx(assign2, support, !assignment.empty());        
@@ -296,20 +408,20 @@ struct mus::imp {
         return is_sat;
     }
 
-    void get_core(uint_set& core) {
+    void get_core(expr_set& core) {
+        core.reset();
         ptr_vector<expr> core_exprs;
-        unsigned lit_id;
         m_solver.get_unsat_core(core_exprs);
         for (unsigned i = 0; i < core_exprs.size(); ++i) {
-            if (m_expr2lit.find(core_exprs[i], lit_id)) {
-                core.insert(lit_id);
+            if (m_expr2lit.contains(core_exprs[i])) {
+                core.insert(core_exprs[i]);
             }
         }
     }
 
-    void unsplit(uint_set& A, uint_set& B) {
-        uint_set A1, B1;
-        uint_set::iterator it = A.begin(), end = A.end();
+    void unsplit(expr_set& A, expr_set& B) {
+        expr_set A1, B1;
+        expr_set::iterator it = A.begin(), end = A.end();
         for (; it != end; ++it) {
             if (B.contains(*it)) {
                 B1.insert(*it);
@@ -322,10 +434,10 @@ struct mus::imp {
         B = B1;
     }
 
-    void split(uint_set& lits1, uint_set& lits2) {
-        unsigned half = lits1.num_elems()/2;
-        uint_set lits3;
-        uint_set::iterator it = lits1.begin(), end = lits1.end();
+    void split(expr_set& lits1, expr_set& lits2) {
+        unsigned half = lits1.size()/2;
+        expr_set lits3;
+        expr_set::iterator it = lits1.begin(), end = lits1.end();
         for (unsigned i = 0; it != end; ++it, ++i) {
             if (i < half) {
                 lits3.insert(*it);
@@ -355,7 +467,11 @@ void mus::add_assumption(expr* lit) {
     return m_imp->add_assumption(lit);
 }
 
-lbool mus::get_mus(unsigned_vector& mus) {
+lbool mus::get_mus(ptr_vector<expr>& mus) {
+    return m_imp->get_mus(mus);
+}
+
+lbool mus::get_mus(expr_ref_vector& mus) {
     return m_imp->get_mus(mus);
 }
 
diff --git a/src/solver/mus.h b/src/solver/mus.h
index d2411b6ec..f2e543f04 100644
--- a/src/solver/mus.h
+++ b/src/solver/mus.h
@@ -33,6 +33,10 @@ class mus {
        Assume also that cls is a literal.           
     */
     unsigned add_soft(expr* cls);
+
+    void add_soft(unsigned sz, expr* const* clss) {
+        for (unsigned i = 0; i < sz; ++i) add_soft(clss[i]);
+    }
     
     /**
        Additional assumption for solver to be used along with solver context, 
@@ -43,7 +47,9 @@ class mus {
      */
     void add_assumption(expr* lit);
 
-    lbool get_mus(unsigned_vector& mus);
+    lbool get_mus(ptr_vector<expr>& mus);
+
+    lbool get_mus(expr_ref_vector& mus);
     
     void reset();
     
diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h
index 019468fd7..9aeb56fb1 100644
--- a/src/solver/solver_na2as.h
+++ b/src/solver/solver_na2as.h
@@ -25,6 +25,7 @@ Notes:
 #include"solver.h"
 
 class solver_na2as : public solver {
+ protected:
     ast_manager &      m;
     expr_ref_vector    m_assumptions;
     unsigned_vector    m_scopes;
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 488157c00..fe51963e0 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -556,6 +556,38 @@ public:
         out << "]";
     }
 
+    core_hashtable& operator|=(core_hashtable const& other) {
+        if (this == &other) return *this;
+        iterator i = begin(), e = end();
+        for (; i != e; ++i) {
+            insert(*i);
+        }
+        return *this;
+    }
+
+
+    core_hashtable& operator&=(core_hashtable const& other) {
+        if (this == &other) return *this;
+        core_hashtable copy(*this);
+        iterator i = copy.begin(), e = copy.end();
+        for (; i != e; ++i) {
+            if (!other.contains(*i)) {
+                remove(*i);
+            }
+        }
+        return *this;
+    }
+
+    core_hashtable& operator=(core_hashtable const& other) {
+        if (this == &other) return *this;
+        reset();
+        core_hashtable::iterator i = other.begin(), e = other.end();
+        for (; i != e; ++i) {
+            insert(*i);
+        }
+        return *this;
+    }
+
 #ifdef Z3DEBUG
     bool check_invariant() {
         entry * curr = m_table;
@@ -582,9 +614,6 @@ public:
     unsigned long long get_num_collision() const { return 0; }
 #endif
 
- private:
-
-    core_hashtable& operator=(core_hashtable const&);
     
 };
 
@@ -640,4 +669,5 @@ public:
         core_hashtable<int_hash_entry<INT_MIN, INT_MIN + 1>, HashProc, EqProc>(initial_capacity, h, e) {}
 };
 
+
 #endif /* HASHTABLE_H_ */
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 4e948d96d..383ecaeb3 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -51,6 +51,7 @@ class obj_hashtable : public core_hashtable<obj_hash_entry<T>, obj_ptr_hash<T>,
 public:
     obj_hashtable(unsigned initial_capacity = DEFAULT_HASHTABLE_INITIAL_CAPACITY):
         core_hashtable<obj_hash_entry<T>, obj_ptr_hash<T>, ptr_eq<T> >(initial_capacity) {}
+
 };
 
 template<typename Key, typename Value>