diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp
index ae4c657bd..9110014bf 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -276,8 +276,8 @@ expr * func_interp::get_interp() const {
     return r;
 }
 
-func_interp * func_interp::translate(ast_translation & translator) const {
-    func_interp * new_fi = alloc(func_interp, m_manager, m_arity);
+func_interp * func_interp::translate(ast_translation & translator) const {    
+    func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
 
     ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
     ptr_vector<func_entry>::const_iterator end = m_entries.end();
diff --git a/src/model/model.cpp b/src/model/model.cpp
index a6b9695b4..73a39a8eb 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -74,6 +74,7 @@ void model::register_decl(func_decl * d, expr * v) {
 
 void model::register_decl(func_decl * d, func_interp * fi) {
     SASSERT(d->get_arity() > 0);
+    SASSERT(&fi->m() == &m_manager);
     decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, 0);
     if (entry->get_data().m_value == 0) {
         // new entry