diff --git a/src/model/model.cpp b/src/model/model.cpp
index 023502485..b14887027 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -63,7 +63,7 @@ void model::updt_params(params_ref const & p) {
 
 void model::copy_const_interps(model const & source) {
     for (auto const& kv : source.m_interp) 
-        register_decl(kv.m_key, kv.m_value);
+        register_decl(kv.m_key, kv.m_value.second);
 }
 
 void model::copy_func_interps(model const & source) {
@@ -168,12 +168,14 @@ model * model::translate(ast_translation & translator) const {
 
     // Translate const interps
     for (auto const& kv : m_interp) {
-        res->register_decl(translator(kv.m_key), translator(kv.m_value));
+        func_decl_ref d(translator(kv.m_key), translator.to());
+        expr_ref v(translator(kv.m_value.second), translator.to());
+        res->register_decl(d, v);
     }
     // Translate func interps
     for (auto const& kv : m_finterp) {
-        func_interp * fi = kv.m_value;
-        res->register_decl(translator(kv.m_key), fi->translate(translator));
+        func_interp* fi = kv.m_value->translate(translator);
+        res->register_decl(translator(kv.m_key), fi);
     }
 
     // Translate usort interps
@@ -265,7 +267,7 @@ void model::collect_deps(top_sort& ts) {
         ts.insert(kv.m_key, collect_deps(ts, kv.m_value));
     }
     for (auto const& kv : m_interp) {
-        ts.insert(kv.m_key, collect_deps(ts, kv.m_value));
+        ts.insert(kv.m_key, collect_deps(ts, kv.m_value.second));
     }
 }
 
diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index bfcd43f9f..fcddce59f 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -22,7 +22,7 @@ Revision History:
 model_core::~model_core() {
     for (auto & kv : m_interp) {
         m.dec_ref(kv.m_key);
-        m.dec_ref(kv.m_value);
+        m.dec_ref(kv.m_value.second);
     }
 
     for (auto & kv : m_finterp) {
@@ -56,20 +56,22 @@ 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";
           );
-    auto& value = m_interp.insert_if_not_there(d, nullptr);
-    if (value == nullptr) {
+    i_expr v0(0, nullptr);
+    auto& value = m_interp.insert_if_not_there(d, v0);
+    if (value == v0) {
         // new entry
-        m_decls.push_back(d);
-        m_const_decls.push_back(d);
         m.inc_ref(d);
         m.inc_ref(v);
-        value = v;
+        value.second = v;
+        value.first = m_const_decls.size();
+        m_decls.push_back(d);
+        m_const_decls.push_back(d);
     }
     else {
         // replacing entry
         m.inc_ref(v);
-        m.dec_ref(value);
-        value = v;
+        m.dec_ref(value.second);
+        value.second = v;
     }
 }
 
@@ -104,10 +106,12 @@ void model_core::unregister_decl(func_decl * d) {
     if (ec) {
         auto k = ec->get_data().m_key;
         auto v = ec->get_data().m_value;
+        m_const_decls[v.first] = m_const_decls.back();
+        m_interp[m_const_decls.back()].first = v.first;
+        m_const_decls.pop_back();
         m_interp.remove(d);
-        m_const_decls.erase(d);
         m.dec_ref(k);
-        m.dec_ref(v);
+        m.dec_ref(v.second);
         return;
     }
 
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 70c5e34d6..8e531a2b6 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -24,7 +24,9 @@ Revision History:
 
 class model_core {
 protected:
-    typedef obj_map<func_decl, expr *>       decl2expr;
+    typedef std::pair<unsigned, expr*> i_expr;
+    typedef std::pair<unsigned, func_interp*> i_interp;
+    typedef obj_map<func_decl, i_expr>       decl2expr;
     typedef obj_map<func_decl, func_interp*> decl2finterp;
     ast_manager &                 m;
     unsigned                      m_ref_count;
@@ -43,7 +45,7 @@ public:
     unsigned get_num_decls() const { return m_decls.size(); }
     func_decl * get_decl(unsigned i) const { return m_decls[i]; }
     bool has_interpretation(func_decl * d) const { return m_interp.contains(d) || m_finterp.contains(d); }
-    expr * get_const_interp(func_decl * d) const { expr * v; return m_interp.find(d, v) ? v : nullptr; }
+    expr * get_const_interp(func_decl * d) const { i_expr v; return m_interp.find(d, v) ? v.second : nullptr; }
     func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; }
 
     bool eval(func_decl * f, expr_ref & r) const;
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 816047f49..d0ec5cd1f 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -220,7 +220,7 @@ void proto_model::cleanup() {
     }
     for (unsigned i = 0; i < m_const_decls.size(); ++i) {
         func_decl* d = m_const_decls[i];
-        expr* e = m_interp[d];
+        expr* e = m_interp[d].second;
         expr* r = cleanup_expr(trail, e, found_aux_fs);
         if (e != r) {
             register_decl(d, r);
@@ -385,7 +385,7 @@ model * proto_model::mk_model() {
     model * mdl = alloc(model, m);
 
     for (auto const& kv : m_interp) {
-        mdl->register_decl(kv.m_key, kv.m_value);
+        mdl->register_decl(kv.m_key, kv.m_value.second);
     }
 
     for (auto const& kv : m_finterp) {
diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp
index a64a3a79d..bf04a3ee2 100644
--- a/src/tactic/generic_model_converter.cpp
+++ b/src/tactic/generic_model_converter.cpp
@@ -108,7 +108,17 @@ model_converter * generic_model_converter::translate(ast_translation & translato
     ast_manager& to = translator.to();
     generic_model_converter * res = alloc(generic_model_converter, to, m_orig.c_str());
     for (entry const& e : m_entries) {
-        res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
+        func_decl_ref d(translator(e.m_f.get()), to);
+        switch (e.m_instruction) {
+        case instruction::HIDE: 
+            res->hide(d);
+            break;        
+        case instruction::ADD: {
+            expr_ref def(translator(e.m_def.get()), to);            
+            res->add(d, def);
+            break;
+        }
+        }
     }
     return res;
 }