diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index b524cd8d4..c27651fca 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1532,6 +1532,17 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
               tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
           });
     ast_translation trans(const_cast<ast_manager&>(from), *this, false);
+    // Inheriting plugins can create new family ids. Since new family ids are
+    // assigned in the order that they are created, this can result in differing
+    // family ids. To avoid this, we first assign all family ids and only then inherit plugins.
+    for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
+      symbol fid_name   = from.get_family_name(fid);
+      if (!m_family_manager.has_family(fid)) {
+          family_id new_fid = mk_family_id(fid_name);
+          (void)new_fid;
+          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
+      }
+    }
     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));
@@ -1539,11 +1550,6 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
       TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
             << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
             if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
-      if (!m_family_manager.has_family(fid)) {
-          family_id new_fid = mk_family_id(fid_name);
-          (void)new_fid;
-          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
-      }
       TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
       SASSERT(fid == get_family_id(fid_name));
       if (from.has_plugin(fid) && !has_plugin(fid)) {