diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a905efa28..bb81c1eba 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1529,12 +1529,15 @@ void ast_manager::raise_exception(char const * msg) {
     throw ast_exception(msg);
 }
 
+#include "ast/ast_translation.h"
+
 void ast_manager::copy_families_plugins(ast_manager const & from) {
     TRACE("copy_families_plugins",
           tout << "target:\n";
           for (family_id fid = 0; m_family_manager.has_family(fid); fid++) {
               tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
           });
+    ast_translation trans(const_cast<ast_manager&>(from), *this, false);
     for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
       SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
       SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
@@ -1555,6 +1558,9 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
           SASSERT(new_p->get_family_id() == fid);
           SASSERT(has_plugin(fid));
       }
+      if (from.has_plugin(fid)) {
+          get_plugin(fid)->inherit(from.get_plugin(fid), trans);
+      }
       SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
       SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
       SASSERT(!from.has_plugin(fid) || has_plugin(fid));
diff --git a/src/ast/ast.h b/src/ast/ast.h
index a1e31f46f..4eb43d30b 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -895,6 +895,8 @@ struct ast_eq_proc {
     }
 };
 
+class ast_translation;
+
 class ast_table : public chashtable<ast*, obj_ptr_hash<ast>, ast_eq_proc> {
 public:
     void erase(ast * n);
@@ -930,6 +932,8 @@ protected:
         m_family_id = id;
     }
 
+    virtual void inherit(decl_plugin* other_p, ast_translation& ) { }
+
     friend class ast_manager;
 
 public:
diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp
index 0c56b6de6..1bce4bcbe 100644
--- a/src/ast/ast_translation.cpp
+++ b/src/ast/ast_translation.cpp
@@ -37,11 +37,9 @@ void ast_translation::cleanup() {
 }
 
 void ast_translation::reset_cache() {
-    obj_map<ast, ast*>::iterator it  = m_cache.begin();
-    obj_map<ast, ast*>::iterator end = m_cache.end();
-    for (; it != end; ++it) {
-        m_from_manager.dec_ref(it->m_key);
-        m_to_manager.dec_ref(it->m_value);
+    for (auto & kv : m_cache) {
+        m_from_manager.dec_ref(kv.m_key);
+        m_to_manager.dec_ref(kv.m_value);
     }
     m_cache.reset();
 }
diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp
index 43164a436..0a002ed08 100644
--- a/src/ast/datatype_decl_plugin2.cpp
+++ b/src/ast/datatype_decl_plugin2.cpp
@@ -24,6 +24,7 @@ Revision History:
 #include "ast/datatype_decl_plugin2.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_translation.h"
 
 
 namespace datatype {
@@ -53,6 +54,9 @@ namespace datatype {
 
     def const& accessor::get_def() const { return m_constructor->get_def(); }
     util& accessor::u() const { return m_constructor->u(); }
+    accessor* accessor::translate(ast_translation& tr) {
+        return alloc(accessor, tr.to(), name(), to_sort(tr(m_range.get())));
+    }
 
     constructor::~constructor() {
         for (accessor* a : m_accessors) dealloc(a);
@@ -76,6 +80,15 @@ namespace datatype {
         return instantiate(sorts);
     }
 
+    constructor* constructor::translate(ast_translation& tr) {
+        constructor* result = alloc(constructor, m_name, m_recognizer);
+        for (accessor* a : *this) {
+            result->add(a->translate(tr));
+        }
+        return result;
+    }
+
+
     sort_ref def::instantiate(sort_ref_vector const& sorts) const {
         sort_ref s(m);
         TRACE("datatype", tout << "instantiate " << m_name << "\n";);
@@ -91,6 +104,19 @@ namespace datatype {
         return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m);
     }
 
+    def* def::translate(ast_translation& tr, util& u) {
+        sort_ref_vector ps(tr.to());
+        for (sort* p : m_params) {
+            ps.push_back(to_sort(tr(p)));
+        }
+        def* result = alloc(def, tr.to(), u, m_name, m_class_id, ps.size(), ps.c_ptr());
+        for (constructor* c : *this) {
+            add(c->translate(tr));
+        }
+        if (m_sort) result->m_sort = to_sort(tr(m_sort.get()));
+        return result;               
+    }
+
     enum status {
         GRAY,
         BLACK
@@ -145,6 +171,27 @@ namespace datatype {
             return *(m_util.get());
         }
 
+        static unsigned stack_depth = 0;
+
+        void plugin::inherit(decl_plugin* other_p, ast_translation& tr) {
+            ++stack_depth;
+            SASSERT(stack_depth < 10);
+            plugin* p = dynamic_cast<plugin*>(other_p);
+            svector<symbol> names;
+            SASSERT(p);
+            for (auto& kv : p->m_defs) {
+                def* d = kv.m_value;
+                if (!m_defs.contains(kv.m_key)) {
+                    names.push_back(kv.m_key);
+                    m_defs.insert(kv.m_key, d->translate(tr, u()));
+                }
+            }
+            m_class_id = m_defs.size();
+            u().compute_datatype_size_functions(names);
+            --stack_depth;
+        }
+
+
         struct invalid_datatype {};
 
         sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h
index a88c7100e..364ba9350 100644
--- a/src/ast/datatype_decl_plugin2.h
+++ b/src/ast/datatype_decl_plugin2.h
@@ -75,6 +75,7 @@ namespace datatype {
         constructor const& get_constructor() const { return *m_constructor; }
         def const& get_def() const;
         util& u() const;
+        accessor* translate(ast_translation& tr);
     };
 
     class constructor {
@@ -98,6 +99,7 @@ namespace datatype {
         void attach(def* d) { m_def = d; }
         def const& get_def() const { return *m_def; }
         util& u() const;
+        constructor* translate(ast_translation& tr);
     };
 
     namespace param_size {
@@ -228,6 +230,7 @@ namespace datatype {
         util& u() const { return m_util; }
         param_size::size* sort_size() { return m_sort_size; }
         void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = 0; }
+        def* translate(ast_translation& tr, util& u);
     };
 
     namespace decl {
@@ -238,6 +241,9 @@ namespace datatype {
             svector<symbol>          m_def_block;
             unsigned                 m_class_id;
             util & u() const;
+
+            virtual void inherit(decl_plugin* other_p, ast_translation& tr);
+
         public:
             plugin(): m_class_id(0) {}
             virtual ~plugin();
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 9d86436d9..36272a139 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -61,15 +61,14 @@ namespace smt {
         }
 
         virtual solver * translate(ast_manager & m, params_ref const & p) {
+            ast_translation translator(get_manager(), m);
+
             solver * result = alloc(solver, m, p, m_logic);
             smt::kernel::copy(m_context, result->m_context);
 
-            ast_translation translator(get_manager(), m);
-            obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
-            obj_map<expr, expr*>::iterator end = m_name2assertion.end();
-            for (; it != end; it++)
-                result->m_name2assertion.insert(translator(it->m_key),
-                                                translator(it->m_value));
+            for (auto & kv : m_name2assertion) 
+                result->m_name2assertion.insert(translator(kv.m_key),
+                                                translator(kv.m_value));
 
             return result;
         }
@@ -264,7 +263,7 @@ namespace smt {
         }
 
         void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
-            assrtn_fds.resize(m_name2assertion.size());
+            assrtn_fds.resize(m_name2assertion.size());            
             obj_map<expr, expr*>::iterator ait = m_name2assertion.begin();
             obj_map<expr, expr*>::iterator aend = m_name2assertion.end();
             for (unsigned i = 0; ait != aend; ait++, i++) {
@@ -277,10 +276,7 @@ namespace smt {
         }
 
         bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) {
-            func_decl_set::iterator it = pattern_fds.begin();
-            func_decl_set::iterator end = pattern_fds.end();
-            for (; it != end; it++) {
-                func_decl * fd = *it;
+            for (func_decl * fd : pattern_fds) {
                 if (assrtn_fds.contains(fd))
                     return true;
             }