diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp
index aaece1621..72bf0d7a8 100644
--- a/src/api/api_ast_map.cpp
+++ b/src/api/api_ast_map.cpp
@@ -86,18 +86,18 @@ extern "C" {
         LOG_Z3_ast_map_insert(c, m, k, v);
         RESET_ERROR_CODE();
         ast_manager & mng = to_ast_map(m)->m;
-        obj_map<ast, ast*>::obj_map_entry * entry = to_ast_map_ref(m).insert_if_not_there2(to_ast(k), 0);
-        if (entry->get_data().m_value == 0) {
+        auto& value = to_ast_map_ref(m).insert_if_not_there(to_ast(k), 0);
+        if (!value) {
             // new entry
             mng.inc_ref(to_ast(k));
             mng.inc_ref(to_ast(v));
-            entry->get_data().m_value = to_ast(v);            
+            value = to_ast(v);            
         }
         else {
             // replacing entry
             mng.inc_ref(to_ast(v));
-            mng.dec_ref(entry->get_data().m_value);
-            entry->get_data().m_value = to_ast(v);
+            mng.dec_ref(value);
+            value = to_ast(v);
         }
         Z3_CATCH;
     }
diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index a3d37171d..957b884fb 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -65,14 +65,14 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 }
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
-    obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    expr*& value = m_subst.insert_if_not_there(c, nullptr); 
     SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(0) == c);
     SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(1) == def);
-    if (entry->get_data().m_value == nullptr) {
+    if (value == nullptr) {
         // new entry
         m_manager.inc_ref(c);
         m_manager.inc_ref(def);
-        entry->get_data().m_value = def;
+        value = def;
         if (proofs_enabled()) {
             SASSERT(!m_subst_pr->contains(c));
             m_subst_pr->insert(c, def_pr);
@@ -87,8 +87,8 @@ void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_depend
     else {
         // replacing entry
         m_manager.inc_ref(def);
-        m_manager.dec_ref(entry->get_data().m_value);
-        entry->get_data().m_value = def;
+        m_manager.dec_ref(value);
+        value = def;
         if (proofs_enabled()) {
             obj_map<expr, proof*>::obj_map_entry * entry_pr = m_subst_pr->find_core(c);
             SASSERT(entry_pr != nullptr);
diff --git a/src/ast/macro_substitution.cpp b/src/ast/macro_substitution.cpp
index 2868a1876..cb85584b1 100644
--- a/src/ast/macro_substitution.cpp
+++ b/src/ast/macro_substitution.cpp
@@ -82,12 +82,12 @@ void macro_substitution::insert(func_decl * f, quantifier * q, proof * pr, expr_
         expr * rhs = body->get_arg(1);
         SASSERT(is_app_of(lhs, f) || is_app_of(rhs, f));
     });
-    obj_map<func_decl, quantifier *>::obj_map_entry * entry = m_decl2macro.insert_if_not_there2(f, 0); 
-    if (entry->get_data().m_value == 0) {
+    quantifier*& entry = m_decl2macro.insert_if_not_there(f, 0); 
+    if (entry == nullptr) {
         // new entry
         m_manager.inc_ref(f);
         m_manager.inc_ref(q);
-        entry->get_data().m_value = q;
+        entry = q;
         if (proofs_enabled()) {
             SASSERT(!m_decl2macro_pr->contains(f));
             m_decl2macro_pr->insert(f, pr);
@@ -102,8 +102,8 @@ void macro_substitution::insert(func_decl * f, quantifier * q, proof * pr, expr_
     else {
         // replacing entry
         m_manager.inc_ref(q);
-        m_manager.dec_ref(entry->get_data().m_value);
-        entry->get_data().m_value = q;
+        m_manager.dec_ref(entry);
+        entry = q;
         if (proofs_enabled()) {
             obj_map<func_decl, proof *>::obj_map_entry * entry_pr = m_decl2macro_pr->find_core(f);
             SASSERT(entry_pr != 0);
diff --git a/src/ast/num_occurs.cpp b/src/ast/num_occurs.cpp
index 2448dd081..f3f8f2914 100644
--- a/src/ast/num_occurs.cpp
+++ b/src/ast/num_occurs.cpp
@@ -24,8 +24,7 @@ void num_occurs::process(expr * t, expr_fast_mark1 & visited) {
     
 #define VISIT(ARG) {                                                                                    \
         if (!m_ignore_ref_count1 || ARG->get_ref_count() > 1) {                                         \
-            obj_map<expr, unsigned>::obj_map_entry * entry = m_num_occurs.insert_if_not_there2(ARG, 0); \
-            entry->get_data().m_value++;                                                                \
+            m_num_occurs.insert_if_not_there(ARG, 0)++; \
         }                                                                                               \
         if (!visited.is_marked(ARG)) {                                                                  \
             visited.mark(ARG, true);                                                                    \
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 651ecce10..a26e486ce 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -458,10 +458,10 @@ namespace recfun {
             for (expr* t : subterms(tmp)) {
                 if (is_app(t)) {
                     for (expr* arg : *to_app(t)) {
-                        parents.insert_if_not_there2(arg, ptr_vector<expr>())->get_data().m_value.push_back(t);        
+                        parents.insert_if_not_there(arg, ptr_vector<expr>()).push_back(t);        
                     }
                 }
-                by_depth.insert_if_not_there2(get_depth(t), ptr_vector<expr>())->get_data().m_value.push_back(t);
+                by_depth.insert_if_not_there(get_depth(t), ptr_vector<expr>()).push_back(t);
             }
             unsigned max_depth = get_depth(e);
             scores.insert(e, 0);
diff --git a/src/ast/rewriter/ast_counter.cpp b/src/ast/rewriter/ast_counter.cpp
index bc11e4fb0..0e89f8228 100644
--- a/src/ast/rewriter/ast_counter.cpp
+++ b/src/ast/rewriter/ast_counter.cpp
@@ -25,11 +25,11 @@ void counter::update(unsigned el, int delta) {
 }
 
 int & counter::get(unsigned el) {
-    return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+    return m_data.insert_if_not_there(el, 0);
 }
 
 counter & counter::count(unsigned sz, const unsigned * els, int delta) {
-    for(unsigned i=0; i<sz; i++) {
+    for(unsigned i = 0; i < sz; i++) {
         update(els[i], delta);
     }
     return *this;
@@ -37,32 +37,24 @@ counter & counter::count(unsigned sz, const unsigned * els, int delta) {
 
 unsigned counter::get_positive_count() const {
     unsigned cnt = 0;
-    iterator eit = begin();
-    iterator eend = end();
-    for(; eit!=eend; ++eit) {
-        if( eit->m_value>0 ) { 
+    for (auto const& kv : *this)
+        if (kv.m_value > 0) 
             cnt++;
-        }
-    }
     return cnt;
 }
 
 void counter::collect_positive(uint_set & acc) const {
-    iterator eit = begin();
-    iterator eend = end();
-    for(; eit!=eend; ++eit) {
-        if(eit->m_value>0) { acc.insert(eit->m_key); }
-    }
+    for (auto const& kv : *this) 
+        if(kv.m_value > 0) 
+            acc.insert(kv.m_key); 
 }
 
 bool counter::get_max_positive(unsigned & res) const {
     bool found = false;
-    iterator eit = begin();
-    iterator eend = end();
-    for(; eit!=eend; ++eit) {
-        if( eit->m_value>0 && (!found || eit->m_key>res) ) { 
+    for (auto const& kv : *this) {
+        if (kv.m_value > 0 && (!found || kv.m_key > res) ) { 
             found = true;
-            res = eit->m_key;
+            res = kv.m_key;
         }
     }
     return found;
@@ -76,12 +68,9 @@ unsigned counter::get_max_positive() const {
 
 int counter::get_max_counter_value() const {
     int res = 0;
-    iterator eit = begin();
-    iterator eend = end();
-    for (; eit!=eend; ++eit) {
-        if( eit->m_value>res ) { 
-            res = eit->m_value;
-        }
+    for (auto const& kv : *this) {
+        if (kv.m_value > res) 
+            res = kv.m_value;
     }
     return res;
 }
diff --git a/src/ast/rewriter/ast_counter.h b/src/ast/rewriter/ast_counter.h
index a2d1c239b..b6e6b0dd4 100644
--- a/src/ast/rewriter/ast_counter.h
+++ b/src/ast/rewriter/ast_counter.h
@@ -93,7 +93,7 @@ class ast_counter {
     iterator end() const { return m_data.end(); }
     
     int & get(ast * el) {
-        return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+        return m_data.insert_if_not_there(el, 0);
     }
     void update(ast * el, int delta){
         get(el) += delta;
diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp
index df3186df4..989d96d25 100644
--- a/src/ast/rewriter/bv_bounds.cpp
+++ b/src/ast/rewriter/bv_bounds.cpp
@@ -523,10 +523,10 @@ bool bv_bounds::bound_lo(app * v, const numeral& l) {
     SASSERT(in_range(v, l));
     TRACE("bv_bounds", tout << "lower " << mk_ismt2_pp(v, m_m) << ":" << l << std::endl;);
     // l <= v
-    bound_map::obj_map_entry * const entry = m_unsigned_lowers.insert_if_not_there2(v, l);
-    if (!(entry->get_data().m_value < l)) return m_okay;
+    auto& value = m_unsigned_lowers.insert_if_not_there(v, l);
+    if (!(value < l)) return m_okay;
     // improve bound
-    entry->get_data().m_value = l;
+    value = l;
     return m_okay;
 }
 
@@ -534,10 +534,10 @@ bool bv_bounds::bound_up(app * v, const numeral& u) {
     SASSERT(in_range(v, u));
     TRACE("bv_bounds", tout << "upper " << mk_ismt2_pp(v, m_m) << ":" << u << std::endl;);
     // v <= u
-    bound_map::obj_map_entry * const entry = m_unsigned_uppers.insert_if_not_there2(v, u);
-    if (!(u < entry->get_data().m_value)) return m_okay;
+    auto& value = m_unsigned_uppers.insert_if_not_there(v, u);
+    if (!(u < value)) return m_okay;
     // improve bound
-    entry->get_data().m_value = u;
+    value = u;
     return m_okay;
 }
 
diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp
index abcdabc9c..2a1c7217d 100644
--- a/src/ast/rewriter/factor_rewriter.cpp
+++ b/src/ast/rewriter/factor_rewriter.cpp
@@ -341,11 +341,8 @@ bool factor_rewriter::extract_factors() {
 
 void factor_rewriter::collect_powers() {
     m_powers.reset();
-    for (unsigned i = 0; i < m_factors.size(); ++i) {
-        obj_map<expr,unsigned>::obj_map_entry* entry = m_powers.insert_if_not_there2(m_factors[i].get(), 0);
-        if (entry) {
-            ++(entry->get_data().m_value);
-        }
+    for (expr* f : m_factors) {
+        m_powers.insert_if_not_there(f, 0)++;
     }
 }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 518926e0c..8a3a44093 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1326,7 +1326,7 @@ seq_rewriter::length_comparison seq_rewriter::compare_lengths(unsigned sza, expr
         if (m_util.str.is_unit(as[i]))
             units_a++;
         else 
-            mults.insert_if_not_there2(as[i], 0)->get_data().m_value++;
+            mults.insert_if_not_there(as[i], 0)++;
     }
     for (unsigned i = 0; i < szb; ++i) {
         if (m_util.str.is_unit(bs[i]))
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 848ee02da..efccdd434 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -793,8 +793,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
         throw cmd_exception("invalid declaration, builtin symbol ", s);
     }
 #endif
-    dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
-    func_decls & fs = e->get_data().m_value;
+    func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls());
     if (!fs.insert(m(), f)) {
         std::string msg = "invalid declaration, ";
         msg += f->get_arity() == 0 ? "constant" : "function";
@@ -877,8 +876,7 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
     if (!m_mc0.get()) m_mc0 = alloc(generic_model_converter, m(), "cmd_context");
     if (m_solver.get() && !m_solver->mc0()) m_solver->set_model_converter(m_mc0.get()); 
     func_decl_ref fn(m().mk_func_decl(s, arity, domain, m().get_sort(t)), m());
-    dictionary<func_decls>::entry * e = m_func_decls.insert_if_not_there2(s, func_decls());
-    func_decls & fs = e->get_data().m_value;
+    func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls());
     fs.insert(m(), fn);
     VERIFY(fn->get_range() == m().get_sort(t));
     m_mc0->add(fn, t);
diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp
index 4d44b1b80..c107c8dec 100644
--- a/src/math/grobner/pdd_simplifier.cpp
+++ b/src/math/grobner/pdd_simplifier.cpp
@@ -191,8 +191,7 @@ namespace dd {
         for (equation* eq1 : s.m_to_simplify) {
             SASSERT(eq1->state() == solver::to_simplify);
             pdd p = eq1->poly();
-            auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
-            equation* eq2 = e->get_data().m_value;
+            equation* eq2 = los.insert_if_not_there(p.lo().index(), eq1);
             pdd q = eq2->poly();
             if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) {
                 *eq1 = p - eq2->poly();
diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index 97c3f0e5c..5b3ae64f0 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -285,8 +285,7 @@ void emonics::insert_cg_mon(monic & m) {
     do_canonize(m);
     lpvar v = m.var(), w;
     TRACE("nla_solver_mons", tout << m << "\n";); //  hash: " << m_cg_hash(v) << "\n";);
-    auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector());
-    auto& vec = entry->get_data().m_value;
+    auto& vec = m_cg_table.insert_if_not_there(v, unsigned_vector());
     if (vec.empty()) {
         vec.push_back(v);
     }
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 60aba6b95..397dfa56c 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -145,15 +145,13 @@ sort * model::get_uninterpreted_sort(unsigned idx) const {
 }
 
 void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
-    sort2universe::obj_map_entry * entry = m_usort2universe.insert_if_not_there2(s, nullptr);
+    ptr_vector<expr>* & u = m_usort2universe.insert_if_not_there(s, nullptr);
     m.inc_array_ref(usize, universe);
-    ptr_vector<expr> * u = entry->get_data().m_value;
     if (!u) {
         m_usorts.push_back(s);
         m.inc_ref(s);
         u = alloc(ptr_vector<expr>);
         u->append(usize, universe);
-        entry->get_data().m_value = u;
     }
     else {
         m.dec_array_ref(u->size(), u->c_ptr());
diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index a3b88b291..97e74f49b 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -56,20 +56,20 @@ void model_core::register_decl(func_decl * d, expr * v) {
     TRACE("model", tout << "register " << d->get_name() << "\n";
           if (v) tout << mk_pp(v, m) << "\n";
           );
-    decl2expr::obj_map_entry * entry = m_interp.insert_if_not_there2(d, nullptr);
-    if (entry->get_data().m_value == nullptr) {
+    auto& value = m_interp.insert_if_not_there(d, nullptr);
+    if (value == nullptr) {
         // new entry
         m_decls.push_back(d);
         m_const_decls.push_back(d);
         m.inc_ref(d);
         m.inc_ref(v);
-        entry->get_data().m_value = v;
+        value = v;
     }
     else {
         // replacing entry
         m.inc_ref(v);
-        m.dec_ref(entry->get_data().m_value);
-        entry->get_data().m_value = v;
+        m.dec_ref(value);
+        value = v;
     }
 }
 
@@ -77,19 +77,19 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
     TRACE("model", tout << "register " << d->get_name() << "\n";);
     SASSERT(d->get_arity() > 0);
     SASSERT(&fi->m() == &m);
-    decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr);
-    if (entry->get_data().m_value == nullptr) {
+    auto& value = m_finterp.insert_if_not_there(d, nullptr);
+    if (value == nullptr) {
         // new entry
         m_decls.push_back(d);
         m_func_decls.push_back(d);
         m.inc_ref(d);
-        entry->get_data().m_value = fi;
+        value = fi;
     }
     else {
         // replacing entry
-        if (fi != entry->get_data().m_value)
-            dealloc(entry->get_data().m_value);
-        entry->get_data().m_value = fi;
+        if (fi != value)
+            dealloc(value);
+        value = fi;
     }
 }
 
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 9d2773326..c9252eece 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -74,8 +74,7 @@ namespace datalog {
 
             unsigned newIdx = m_el_numbers.size();
 
-            sym2num::entry* sym_e = m_el_numbers.insert_if_not_there2(sym, newIdx);
-            unsigned idx=sym_e->get_data().m_value;
+            unsigned idx = m_el_numbers.insert_if_not_there(sym, newIdx);
 
             if (idx==newIdx) {
                 m_el_names.push_back(sym);
@@ -117,10 +116,9 @@ namespace datalog {
 
             unsigned newIdx = m_el_numbers.size();
 
-            el2num::entry* sym_e = m_el_numbers.insert_if_not_there2(el, newIdx);
-            unsigned idx=sym_e->get_data().m_value;
+            unsigned idx = m_el_numbers.insert_if_not_there(el, newIdx);
 
-            if (idx==newIdx) {
+            if (idx == newIdx) {
                 m_el_names.push_back(el);
                 SASSERT(m_el_names.size()==m_el_numbers.size());
             }
@@ -1315,8 +1313,7 @@ namespace datalog {
 
                 // index into fresh variable array.
                 // unsigned fresh_var_idx = 0;
-                obj_map<sort, unsigned_vector>::obj_map_entry* e = var_idxs.insert_if_not_there2(s, unsigned_vector());
-                unsigned_vector& vars = e->get_data().m_value;
+                unsigned_vector& vars = var_idxs.insert_if_not_there(s, unsigned_vector());
                 if (max_var >= vars.size()) {
                     SASSERT(vars.size() == max_var);
                     vars.push_back(fresh_vars.size());
diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 0e5145f66..3a3326903 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -64,11 +64,11 @@ namespace datalog {
     }
 
     rule_dependencies::item_set & rule_dependencies::ensure_key(func_decl * pred) {
-        deps_type::obj_map_entry * e = m_data.insert_if_not_there2(pred, 0);
-        if (!e->get_data().m_value) {
-            e->get_data().m_value = alloc(item_set);
+        auto& value = m_data.insert_if_not_there(pred, 0);
+        if (!value) {
+            value = alloc(item_set);
         }
-        return *e->get_data().m_value;
+        return *value;
     }
 
     void rule_dependencies::insert(func_decl * depending, func_decl * master) {
@@ -324,9 +324,9 @@ namespace datalog {
         app * head = r->get_head();
         SASSERT(head != 0);
         func_decl * d = head->get_decl();
-        decl2rules::obj_map_entry* e = m_head2rules.insert_if_not_there2(d, 0);
-        if (!e->get_data().m_value) e->get_data().m_value = alloc(ptr_vector<rule>);
-        e->get_data().m_value->push_back(r);
+        auto& value = m_head2rules.insert_if_not_there(d, 0);
+        if (!value) value = alloc(ptr_vector<rule>);
+        value->push_back(r);
     }
 
     void rule_set::del_rule(rule * r) {
diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h
index 6f3010940..b906e6c50 100644
--- a/src/muz/dataflow/dataflow.h
+++ b/src/muz/dataflow/dataflow.h
@@ -65,15 +65,15 @@ namespace datalog {
             for (rule* cur : m_rules) {
                 for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) {
                     func_decl *d = cur->get_decl(i);
-                    rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0);
-                    if (!e->get_data().m_value) {
-                        e->get_data().m_value = alloc(ptr_vector<rule>);
+                    auto& value = m_body2rules.insert_if_not_there(d, nullptr);
+                    if (!value) {
+                        value = alloc(ptr_vector<rule>);
                     }
-                    e->get_data().m_value->push_back(cur);
+                    value->push_back(cur);
                 }
                 if (cur->get_positive_tail_size() == 0) {
                     func_decl *sym = cur->get_head()->get_decl();
-                    bool new_info = m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_up(m_context, cur);
+                    bool new_info = m_facts.insert_if_not_there(sym, Fact()).init_up(m_context, cur);
                     if (new_info) {
                         m_todo[m_todo_idx].insert(sym);
                     }
@@ -86,7 +86,7 @@ namespace datalog {
                 TRACE("dl", tout << sym->get_name() << "\n";);
                 const rule_vector& output_rules = m_rules.get_predicate_rules(sym);
                 for (rule* r : output_rules) {
-                    m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, r);
+                    m_facts.insert_if_not_there(sym, Fact()).init_down(m_context, r);
                     m_todo[m_todo_idx].insert(sym);
                 }
             }
@@ -100,7 +100,7 @@ namespace datalog {
                 for (rule* r : *rules) {
                     func_decl* head_sym = r->get_head()->get_decl();
                     fact_reader<Fact> tail_facts(m_facts, r);
-                    bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, r, tail_facts);
+                    bool new_info = m_facts.insert_if_not_there(head_sym, Fact()).propagate_up(m_context, r, tail_facts);
                     if (new_info) {
                         m_todo[!m_todo_idx].insert(head_sym);
                     }
@@ -238,7 +238,7 @@ namespace datalog {
 
         Fact& get(unsigned idx) {
             func_decl *sym = m_rule->get_decl(idx);
-            return m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value;
+            return m_facts.insert_if_not_there(sym, Fact());
         }
 
         void set_changed(unsigned idx) {
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index 45c712f7c..108778fe2 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -1188,11 +1188,11 @@ class wpa_parser_impl : public wpa_parser, dparser {
     bool m_use_map_names;
 
     uint64_set& ensure_sort_content(symbol sort_name) {
-        sym2nums::entry * e = m_sort_contents.insert_if_not_there2(sort_name, nullptr);
-        if(!e->get_data().m_value) {
-            e->get_data().m_value = alloc(uint64_set);
+        auto& value = m_sort_contents.insert_if_not_there(sort_name, nullptr);
+        if (!value) {
+            value = alloc(uint64_set);
         }
-        return *e->get_data().m_value;
+        return *value;
     }
 
 public:        
@@ -1527,10 +1527,10 @@ private:
             sort_elements.insert(num);
             
             if(m_use_map_names) {
-                num2sym::entry * e = m_number_names.insert_if_not_there2(num, el_name);
-                if(e->get_data().m_value!=el_name) {
+                auto const & value = m_number_names.insert_if_not_there(num, el_name);
+                if (value!=el_name) {
                     warning_msg("mismatch of number names on line %d in file %s. old: \"%s\" new: \"%s\"", 
-                        m_current_line, fname.c_str(), e->get_data().m_value.bare_str(), el_name.bare_str());
+                        m_current_line, fname.c_str(), value.bare_str(), el_name.bare_str());
                 }
             }
         }
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index b6f69873b..8604f345d 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -37,15 +37,15 @@ namespace datalog {
     }
 
     void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
-        pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
-        if(e->get_data().m_value!=UINT_MAX) {
+        auto& value = m_pred_regs.insert_if_not_there(pred, UINT_MAX);
+        if (value != UINT_MAX) {
             //predicate is already loaded
             return;
         }
         relation_signature sig;
         m_context.get_rel_context()->get_rmanager().from_predicate(pred, sig);
         reg_idx reg = get_fresh_register(sig);
-        e->get_data().m_value=reg;
+        value = reg;
 
         acc.push_back(instruction::mk_load(m_context.get_manager(), pred, reg));
     }
@@ -570,8 +570,8 @@ namespace datalog {
                 else {
                     SASSERT(is_var(exp));
                     unsigned var_num=to_var(exp)->get_idx();
-                    int2ints::entry * e = var_indexes.insert_if_not_there2(var_num, unsigned_vector());
-                    e->get_data().m_value.push_back(i);
+                    auto& value = var_indexes.insert_if_not_there(var_num, unsigned_vector());
+                    value.push_back(i);
                 }
             }
         }
@@ -631,8 +631,8 @@ namespace datalog {
                     src_col = single_res_expr.size();
                     single_res_expr.push_back(m.mk_var(v, unbound_sort));
 
-                    entry = var_indexes.insert_if_not_there2(v, unsigned_vector());
-                    entry->get_data().m_value.push_back(src_col);
+
+                    var_indexes.insert_if_not_there(v, unsigned_vector()).push_back(src_col);
                 }
                 relation_sort var_sort = m_reg_signatures[filtered_res][src_col];
                 binding[m_free_vars.size()-v] = m.mk_var(src_col, var_sort);
@@ -790,7 +790,7 @@ namespace datalog {
                     unsigned unbound_column_index = single_res_expr.size();
                     single_res_expr.push_back(m.mk_var(v, unbound_sort));
 
-                    e = var_indexes.insert_if_not_there2(v, unsigned_vector());
+                    e = var_indexes.insert_if_not_there3(v, unsigned_vector());
                     e->get_data().m_value.push_back(unbound_column_index);
                 }
                 unsigned src_col=e->get_data().m_value.back();
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index 1c8250a75..76ed1c5bb 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -676,21 +676,21 @@ namespace datalog {
     }
 
     func_decl * mk_explanations::get_e_decl(func_decl * orig_decl) {
-        decl_map::obj_map_entry * e = m_e_decl_map.insert_if_not_there2(orig_decl, 0);
-        if (e->get_data().m_value == nullptr) {
+        auto& value = m_e_decl_map.insert_if_not_there(orig_decl, 0);
+        if (value == nullptr) {
             relation_signature e_domain;
             e_domain.append(orig_decl->get_arity(), orig_decl->get_domain());
             e_domain.push_back(m_e_sort);
             func_decl * new_decl = m_context.mk_fresh_head_predicate(orig_decl->get_name(), symbol("expl"), 
                 e_domain.size(), e_domain.c_ptr(), orig_decl);
             m_pinned.push_back(new_decl);
-            e->get_data().m_value = new_decl;
+            value = new_decl;
 
             if (m_relation_level) {
                 assign_rel_level_kind(new_decl, orig_decl);
             }
         }
-        return e->get_data().m_value;
+        return value;
     }
 
     app * mk_explanations::get_e_lit(app * lit, unsigned e_var_idx) {
diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp
index 7aaf5a533..87ec378ea 100644
--- a/src/muz/rel/dl_mk_simple_joins.cpp
+++ b/src/muz/rel/dl_mk_simple_joins.cpp
@@ -259,8 +259,7 @@ namespace datalog {
             */
         void register_pair(app * t1, app * t2, rule * r, const var_idx_set & non_local_vars) {
             SASSERT (t1 != t2);
-            cost_map::entry * e = m_costs.insert_if_not_there2(get_key(t1, t2), nullptr);
-            pair_info * & ptr_inf = e->get_data().m_value;
+            pair_info * & ptr_inf = m_costs.insert_if_not_there(get_key(t1, t2), nullptr);
             if (ptr_inf == nullptr) {
                 ptr_inf = alloc(pair_info);
             }
@@ -296,8 +295,7 @@ namespace datalog {
             counter.count_rule_vars(r, 1);
             TRACE("dl", tout << "counter: "; for (auto const& kv: counter) tout << kv.m_key << ": " << kv.m_value << " "; tout << "\n";);
 
-            ptr_vector<app> & rule_content = 
-                m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;
+            ptr_vector<app> & rule_content = m_rules_content.insert_if_not_there(r, ptr_vector<app>());
             SASSERT(rule_content.empty());
 
             TRACE("dl", r->display(m_context, tout << "register ");); 
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 48196e874..39255956d 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -105,14 +105,14 @@ namespace datalog {
 
     void relation_manager::store_relation(func_decl * pred, relation_base * rel) {
         SASSERT(rel);
-        relation_map::obj_map_entry * e = m_relations.insert_if_not_there2(pred, 0);
-        if (e->get_data().m_value) {
-            e->get_data().m_value->deallocate();
+        auto& value = m_relations.insert_if_not_there(pred, 0);
+        if (value) {
+            value->deallocate();
         }
         else {
             get_context().get_manager().inc_ref(pred); //dec_ref in reset
         }
-        e->get_data().m_value = rel;
+        value = rel;
     }
 
     decl_set relation_manager::collect_predicates() const {
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index 0fd92b3a7..98e422259 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -673,7 +673,7 @@ namespace datalog {
         family_id get_relation_kind(const relation_signature & sig, const Spec & spec) {
             typename sig2store::entry * e = m_kind_assignment.find_core(sig);
             if(!e) {
-                e = m_kind_assignment.insert_if_not_there2(sig, alloc(family_id_idx_store));
+                e = m_kind_assignment.insert_if_not_there3(sig, alloc(family_id_idx_store));
                 m_kind_specs.insert(sig, alloc(family_id2spec));
             }
             family_id_idx_store & ids = *e->get_data().m_value;
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index db62d14d5..b970d8016 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -302,7 +302,7 @@ namespace datalog {
             index_map::entry * e = m_map.find_core(ofs);
             if (!e) {
                 TRACE("dl_table_relation", tout << "inserting\n";);
-                e = m_map.insert_if_not_there2(ofs, offset_vector());
+                e = m_map.insert_if_not_there3(ofs, offset_vector());
             }
             return e->get_data().m_value;
         }
@@ -473,7 +473,7 @@ namespace datalog {
 #endif
         key_spec kspec;
         kspec.append(key_len, key_cols);
-        key_index_map::entry * key_map_entry = m_key_indexes.insert_if_not_there2(kspec, nullptr);
+        key_index_map::entry * key_map_entry = m_key_indexes.insert_if_not_there3(kspec, nullptr);
         if (!key_map_entry->get_data().m_value) {
             if (full_signature_key_indexer::can_handle(key_len, key_cols, *this)) {
                 key_map_entry->get_data().m_value = alloc(full_signature_key_indexer, key_len, key_cols, *this);
@@ -777,8 +777,7 @@ namespace datalog {
         const table_signature & sig = t->get_signature();
         t->reset();
 
-        table_pool::entry * e = m_pool.insert_if_not_there2(sig, nullptr);
-        sp_table_vector * & vect = e->get_data().m_value;
+        sp_table_vector * & vect = m_pool.insert_if_not_there(sig, nullptr);
         if (vect == nullptr) {
             vect = alloc(sp_table_vector);
         }
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index eb59a06d2..b32756eb0 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2357,10 +2357,10 @@ void context::init_rules(datalog::rule_set& rules, decl2rel& rels)
         func_decl* pred = dit->m_key;
         TRACE("spacer", tout << mk_pp(pred, m) << "\n";);
         SASSERT(!rels.contains(pred));
-        auto *e = rels.insert_if_not_there2(pred, alloc(pred_transformer, *this,
+        auto* pt = rels.insert_if_not_there(pred, alloc(pred_transformer, *this,
                                                         get_manager(), pred));
         datalog::rule_vector const& pred_rules = *dit->m_value;
-        for (auto rule : pred_rules) {e->get_data().m_value->add_rule(rule);}
+        for (auto rule : pred_rules) {pt->add_rule(rule);}
     }
 
     // Allocate predicate transformers for predicates that are used
diff --git a/src/muz/spacer/spacer_pdr.cpp b/src/muz/spacer/spacer_pdr.cpp
index 04b001151..0df9da895 100644
--- a/src/muz/spacer/spacer_pdr.cpp
+++ b/src/muz/spacer/spacer_pdr.cpp
@@ -128,7 +128,7 @@ void model_search::add_leaf(model_node* _n) {
     model_node& n = *_n;
     SASSERT(n.children().empty());
     model_nodes ns;
-    model_nodes& nodes = cache(n).insert_if_not_there2(n.post(), ns)->get_data().m_value;
+    model_nodes& nodes = cache(n).insert_if_not_there(n.post(), ns);
     if (nodes.contains(&n)) return;
 
     nodes.push_back(_n);
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index c1d26b378..15325da43 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -454,9 +454,7 @@ namespace tb {
             unsigned idx = m_rules.size();
             m_rules.push_back(g);
             func_decl* f = g->get_decl();
-            map::obj_map_entry* e = m_index.insert_if_not_there2(f, unsigned_vector());
-            SASSERT(e);
-            e->get_data().m_value.push_back(idx);
+            m_index.insert_if_not_there(f, unsigned_vector()).push_back(idx);
         }
 
         unsigned get_num_rules(func_decl* p) const {
diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp
index 732fd7262..b552f1a06 100644
--- a/src/muz/transforms/dl_mk_filter_rules.cpp
+++ b/src/muz/transforms/dl_mk_filter_rules.cpp
@@ -79,8 +79,7 @@ namespace datalog {
 
         filter_key * key = alloc(filter_key, m);
         mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
-        filter_cache::obj_map_entry *entry = m_tail2filter.insert_if_not_there2(key, 0);
-        func_decl*& filter_decl = entry->get_data().m_value;
+        func_decl*& filter_decl = m_tail2filter.insert_if_not_there(key, 0);
         if (!filter_decl) {
             filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"), 
                 filter_domain.size(), filter_domain.c_ptr(), pred->get_decl());
diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp
index 5ad637c59..b951cfd28 100644
--- a/src/muz/transforms/dl_mk_magic_sets.cpp
+++ b/src/muz/transforms/dl_mk_magic_sets.cpp
@@ -129,15 +129,13 @@ namespace datalog {
         SASSERT(m.is_bool(old_pred->get_range()));
         adornment_desc adn(old_pred);
         adn.m_adornment.populate(lit, bound_vars);
-        adornment_map::entry * e = m_adorned_preds.insert_if_not_there2(adn, nullptr);
-        func_decl * new_pred = e->get_data().m_value;
+        func_decl *& new_pred = m_adorned_preds.insert_if_not_there(adn, nullptr);
         if (new_pred==nullptr) {
             std::string suffix = "ad_"+adn.m_adornment.to_string();
             new_pred = m_context.mk_fresh_head_predicate(
                 old_pred->get_name(), symbol(suffix.c_str()), 
                 old_pred->get_arity(), old_pred->get_domain(), old_pred);
             m_pinned.push_back(new_pred);
-            e->get_data().m_value = new_pred;
             m_todo.push_back(adn);
             m_adornments.insert(new_pred, adn.m_adornment);
         }
@@ -161,8 +159,7 @@ namespace datalog {
             }
         }
 
-        pred2pred::obj_map_entry * e = m_magic_preds.insert_if_not_there2(l_pred, 0);
-        func_decl * mag_pred = e->get_data().m_value;
+        func_decl *& mag_pred = m_magic_preds.insert_if_not_there(l_pred, 0);
         if (mag_pred==nullptr) {
             unsigned mag_arity = bound_args.size();
 
@@ -176,7 +173,6 @@ namespace datalog {
             mag_pred = m_context.mk_fresh_head_predicate(l_pred->get_name(), symbol("ms"), 
                 mag_arity, mag_domain.c_ptr(), l_pred);
             m_pinned.push_back(mag_pred);
-            e->get_data().m_value = mag_pred;
         }
 
         app * res = m.mk_app(mag_pred, bound_args.c_ptr());
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index f06efec6f..504acf753 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -639,9 +639,9 @@ namespace datalog {
     }
 
     unsigned_vector const& mk_rule_inliner::visitor::add_position(expr* e, unsigned j) {
-        obj_map<expr, unsigned_vector>::obj_map_entry * et = m_positions.insert_if_not_there2(e, unsigned_vector());
-        et->get_data().m_value.push_back(j);
-        return et->get_data().m_value;
+        auto& value = m_positions.insert_if_not_there(e, unsigned_vector());
+        value.push_back(j);
+        return value;
     }
 
     unsigned_vector const& mk_rule_inliner::visitor::del_position(expr* e, unsigned j) {
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index 31fd64059..f7925b98b 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -371,8 +371,7 @@ namespace qe {
         for (expr* e : subterms(lits)) {
             if (a.is_int_real(e) && is_uninterp(e) && to_app(e)->get_num_args() > 0) {
                 func_decl* f = to_app(e)->get_decl();
-                auto* v = apps.insert_if_not_there2(f, ptr_vector<app>());
-                v->get_data().m_value.push_back(to_app(e));
+                apps.insert_if_not_there(f, ptr_vector<app>()).push_back(to_app(e));
             }
         }
         for (auto const& kv : apps) {
diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp
index e096e00a3..924630cfb 100644
--- a/src/smt/cached_var_subst.cpp
+++ b/src/smt/cached_var_subst.cpp
@@ -52,7 +52,7 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
     for (unsigned i = 0; i < num_bindings; i++)
         new_key->m_bindings[i] = bindings[i]->get_owner();
 
-    instances::entry * entry = m_instances.insert_if_not_there2(new_key, nullptr);
+    auto* entry = m_instances.insert_if_not_there3(new_key, nullptr);
     if (entry->get_data().m_key != new_key) {
         SASSERT(entry->get_data().m_value != 0);
         // entry was already there
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 1da6a36bd..16cdd91a1 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -201,6 +201,10 @@ namespace smt {
             return m_root; 
         }
 
+        bool is_root() const {
+            return m_root == this;
+        }
+
         void set_root(enode* r) {
             m_root = r;
         }
diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp
index 300280718..494110c49 100644
--- a/src/smt/smt_implied_equalities.cpp
+++ b/src/smt/smt_implied_equalities.cpp
@@ -58,7 +58,7 @@ namespace {
         void partition_terms(unsigned num_terms, expr* const* terms, sort2term_ids& termids) {
             for (unsigned i = 0; i < num_terms; ++i) {
                 sort* s = m.get_sort(terms[i]);
-                term_ids& vec = termids.insert_if_not_there2(s, term_ids())->get_data().m_value;
+                term_ids& vec = termids.insert_if_not_there(s, term_ids());
                 vec.push_back(term_id(expr_ref(terms[i],m), i));
             }
         }
@@ -208,7 +208,7 @@ namespace {
                     continue;
                 }
                 vals.push_back(vl);
-                unsigned_vector& vec = vals_map.insert_if_not_there2(vl, unsigned_vector())->get_data().m_value;
+                unsigned_vector& vec = vals_map.insert_if_not_there(vl, unsigned_vector());
                 bool found = false;
 
                 for (unsigned j = 0; !found && j < vec.size(); ++j) {
diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index cf7dafe89..da2883938 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -132,7 +132,7 @@ namespace smt {
                 return false;
             }
             else {
-                m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
+                m_coeff_map.insert_if_not_there(e, rational(0)) += mul;
             }
         }
         for (auto const& kv : m_coeff_map) {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 36679b1dc..08c8376c8 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -60,12 +60,10 @@ class fix_dl_var_tactic : public tactic {
         
         void inc_occ(expr * n, bool nested) {
             if (is_uninterp_const(n) && is_arith(n)) {
-                obj_map<app, unsigned>::obj_map_entry * entry = m_occs.insert_if_not_there2(to_app(n), 0); 
-                entry->get_data().m_value++;
+                m_occs.insert_if_not_there(to_app(n), 0)++;
 
                 if (!nested) {
-                    entry = m_non_nested_occs.insert_if_not_there2(to_app(n), 0);
-                    entry->get_data().m_value++;
+                    m_non_nested_occs.insert_if_not_there(to_app(n), 0)++;
                 }
             }
         }
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index a87ee2c92..122a376b4 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -101,9 +101,9 @@ class recover_01_tactic : public tactic {
             }
             
             if (x != nullptr) {
-                var2clauses::obj_map_entry * entry = m_var2clauses.insert_if_not_there2(x, ptr_vector<app>());
-                if (entry->get_data().m_value.empty() || entry->get_data().m_value.back()->get_num_args() == cls->get_num_args()) {
-                    entry->get_data().m_value.push_back(cls);
+                auto& value = m_var2clauses.insert_if_not_there(x, ptr_vector<app>());
+                if (value.empty() || value.back()->get_num_args() == cls->get_num_args()) {
+                    value.push_back(cls);
                     return true;
                 }
             }
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index eaa63ac70..949a963ea 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -68,39 +68,39 @@ public:
 
     void update_signed_lower(app * v, numeral const & k) {
         // k <= v
-        obj_map<app, numeral>::obj_map_entry * entry = m_signed_lowers.insert_if_not_there2(v, k);
-        if (entry->get_data().m_value < k) {
+        auto& value = m_signed_lowers.insert_if_not_there(v, k);
+        if (value < k) {
             // improve bound
-            entry->get_data().m_value = k;
+            value = k;
         }
     }
 
     void update_signed_upper(app * v, numeral const & k) {
         // v <= k
-        obj_map<app, numeral>::obj_map_entry * entry = m_signed_uppers.insert_if_not_there2(v, k);
-        if (k < entry->get_data().m_value) {
+        auto& value = m_signed_uppers.insert_if_not_there(v, k);
+        if (k < value) {
             // improve bound
-            entry->get_data().m_value = k;
+            value = k;
         }
     }
     
     void update_unsigned_lower(app * v, numeral const & k) {
         SASSERT(k > numeral(0));
         // k <= v
-        obj_map<app, numeral>::obj_map_entry * entry = m_unsigned_lowers.insert_if_not_there2(v, k);
-        if (entry->get_data().m_value < k) {
+        auto& value = m_unsigned_lowers.insert_if_not_there(v, k);
+        if (value < k) {
             // improve bound
-            entry->get_data().m_value = k;
+            value = k;
         }
     }
 
     void update_unsigned_upper(app * v, numeral const & k) {
         SASSERT(k > numeral(0));
         // v <= k
-        obj_map<app, numeral>::obj_map_entry * entry = m_unsigned_uppers.insert_if_not_there2(v, k);
-        if (k < entry->get_data().m_value) {
+        auto& value = m_unsigned_uppers.insert_if_not_there(v, k);
+        if (k < value) {
             // improve bound
-            entry->get_data().m_value = k;
+            value = k;
         }
     }
 
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 548aacb29..fa9886dbe 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -41,7 +41,7 @@ private:
     tree_t                m_tree;
 
     void add_edge(tree_t& tree, expr * src, expr* dst) {        
-        tree.insert_if_not_there2(src, ptr_vector<expr>())->get_data().m_value.push_back(dst);        
+        tree.insert_if_not_there(src, ptr_vector<expr>()).push_back(dst);        
     }
 
     void compute_post_order();
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index d3fa82ceb..82c06bff8 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -196,7 +196,7 @@ struct reduce_args_tactic::imp {
             expr* base;
             if (it == m_decl2args.end()) {
                 m_decl2args.insert(d, bit_vector());
-                svector<expr*>& bases = m_decl2base.insert_if_not_there2(d, svector<expr*>())->get_data().m_value;
+                svector<expr*>& bases = m_decl2base.insert_if_not_there(d, svector<expr*>());
                 bases.resize(j);
                 it = m_decl2args.find_iterator(d);
                 SASSERT(it != m_decl2args.end());
@@ -347,13 +347,13 @@ struct reduce_args_tactic::imp {
                 return BR_FAILED;
 
             bit_vector & bv = it->m_value;
-            arg2func *& map = m_decl2arg2funcs.insert_if_not_there2(f, 0)->get_data().m_value;
+            arg2func *& map = m_decl2arg2funcs.insert_if_not_there(f, 0);
             if (!map) {
                 map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
             }
 
             app_ref tmp(m.mk_app(f, num, args), m);
-            func_decl *& new_f = map->insert_if_not_there2(tmp, nullptr)->get_data().m_value;
+            func_decl *& new_f = map->insert_if_not_there(tmp, nullptr);
             if (!new_f) {
                 // create fresh symbol
                 ptr_buffer<sort> domain;
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index b6aed81ce..1cd995dc9 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -968,15 +968,14 @@ class solve_eqs_tactic : public tactic {
         void collect_num_occs(expr * t, expr_fast_mark1 & visited) {
             ptr_buffer<expr, 128> stack;
             
-#define VISIT(ARG) {                                                                                            \
-            if (is_uninterp_const(ARG)) {                                                                       \
-                obj_map<expr, unsigned>::obj_map_entry * entry = m_num_occs.insert_if_not_there2(ARG, 0);       \
-                entry->get_data().m_value++;                                                                    \
-            }                                                                                                   \
-            if (!visited.is_marked(ARG)) {                                                                      \
-                visited.mark(ARG, true);                                                                        \
-                stack.push_back(ARG);                                                                           \
-            }                                                                                                   \
+#define VISIT(ARG) {                                                    \
+                if (is_uninterp_const(ARG)) {                           \
+                    m_num_occs.insert_if_not_there(ARG, 0)++;           \
+                }                                                       \
+                if (!visited.is_marked(ARG)) {                          \
+                    visited.mark(ARG, true);                            \
+                    stack.push_back(ARG);                               \
+                }                                                       \
         }
             
             VISIT(t);
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 9e2a0224f..adb669a75 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -282,8 +282,7 @@ private:
             app* t = kv.m_key;
             unsigned n = kv.m_value;
             if (is_uninterpreted(t)) {
-                inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>());
-                e->get_data().m_value.push_back(t);
+                inv_map.insert_if_not_there(n, ptr_vector<app>()).push_back(t);
             }
         }
     }
@@ -346,9 +345,9 @@ private:
             for (unsigned i = 0; i < sz; ++i) {
                 expr* e = n->get_arg(i);
                 if (is_app(e)) {
-                    app_parents::obj_map_entry* entry = m_use_funs.insert_if_not_there2(to_app(e), 0);
-                    if (!entry->get_data().m_value) entry->get_data().m_value = alloc(fun_set);
-                    entry->get_data().m_value->insert(f); 
+                    auto& value = m_use_funs.insert_if_not_there(to_app(e), 0);
+                    if (!value) value = alloc(fun_set);
+                    value->insert(f); 
                 }
             }
         }
@@ -373,14 +372,14 @@ private:
             for (unsigned i = 0; i < sz; ++i) {
                 expr* e = n->get_arg(i);
                 if (!is_app(e)) continue;
-                app_siblings::obj_map_entry* entry = m_sibs.insert_if_not_there2(to_app(e), 0);
-                if (!entry->get_data().get_value()) entry->get_data().m_value = alloc(uint_set);
+                auto& value = m_sibs.insert_if_not_there(to_app(e), 0);
+                if (!value) value = alloc(uint_set);
                 for (unsigned j = 0; j < sz; ++j) {
                     expr* f = n->get_arg(j);
                     if (is_app(f) && i != j) {
                         unsigned c1 = 0;
                         m_colors.find(to_app(f), c1);
-                        entry->get_data().m_value->insert(c1);
+                        value->insert(c1);
                     }
                 }
             }
@@ -517,13 +516,12 @@ private:
         num_occurrences(app_map& occs): m_occs(occs) {}
         void operator()(app* n) {
             app_map::obj_map_entry* e;
-            m_occs.insert_if_not_there2(n, 0);
+            m_occs.insert_if_not_there(n, 0);
             unsigned sz = n->get_num_args();
             for (unsigned i = 0; i < sz; ++i) {
                 expr* arg = n->get_arg(i);
                 if (is_app(arg)) {
-                    e = m_occs.insert_if_not_there2(to_app(arg), 0);
-                    e->get_data().m_value++;
+                    m_occs.insert_if_not_there(to_app(arg), 0)++;
                 }
             }
         }
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index e10c91729..f1a057bc8 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -309,8 +309,7 @@ public:
         unsigned na = n->get_num_args();
         for (unsigned i = 0; i < na; i++) {
             expr * c = n->get_arg(i); 
-            uplinks_type::obj_map_entry * entry = m_uplinks.insert_if_not_there2(c, ptr_vector<expr>());
-            entry->get_data().m_value.push_back(n);
+            m_uplinks.insert_if_not_there(c, ptr_vector<expr>()).push_back(n);
         }
 
         func_decl * d = n->get_decl();
diff --git a/src/util/map.h b/src/util/map.h
index 4ee5139e2..67e794d3f 100644
--- a/src/util/map.h
+++ b/src/util/map.h
@@ -112,11 +112,11 @@ public:
         return m_table.insert_if_not_there_core(key_data(k,v), et);
     }
 
-    key_data const & insert_if_not_there(key const & k, value const & v) {
-        return m_table.insert_if_not_there(key_data(k, v));
+    value & insert_if_not_there(key const & k, value const & v) {
+        return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
     }
     
-    entry * insert_if_not_there2(key const & k, value const & v) {
+    entry * insert_if_not_there3(key const & k, value const & v) {
         return m_table.insert_if_not_there2(key_data(k, v));
     }
         
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index f407120cf..39675fde1 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -146,11 +146,11 @@ public:
         m_table.insert(key_data(k, std::move(v)));
     }
     
-    key_data const & insert_if_not_there(Key * k, Value const & v) {
-        return m_table.insert_if_not_there(key_data(k, v));
+    Value& insert_if_not_there(Key * k, Value const & v) {
+        return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value;
     }
 
-    obj_map_entry * insert_if_not_there2(Key * k, Value const & v) {
+    obj_map_entry * insert_if_not_there3(Key * k, Value const & v) {
         return m_table.insert_if_not_there2(key_data(k, v));
     }
     
diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h
index 2b8924e9f..9856973cf 100644
--- a/src/util/obj_pair_hashtable.h
+++ b/src/util/obj_pair_hashtable.h
@@ -88,6 +88,7 @@ public:
         Key1 * get_key1() const { return m_key1; }
         Key2 * get_key2() const { return m_key2; }
         Value const & get_value() const { return m_value; }
+        Value & get_value() { return m_value; }
     };
 protected:
     class entry {
@@ -149,8 +150,8 @@ public:
         m_table.insert(key_data(k1, k2, v));
     }
     
-    key_data const & insert_if_not_there(Key1 * k1, Key2 * k2, Value const & v) {
-        return m_table.insert_if_not_there(key_data(k1, k2, v));
+    Value& insert_if_not_there(Key1 * k1, Key2 * k2, Value const & v) {
+        return m_table.insert_if_not_there2(key_data(k1, k2, v))->get_data().get_value();
     }
     
     bool find(Key1 * k1, Key2 * k2, Value & v) const {