diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index d875262b3..8a4a0957c 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -321,10 +321,14 @@ namespace datatype {
                         throw invalid_datatype();
                     }
                 }
+
+                def* d = nullptr;
+                if (m_defs.find(name.get_symbol(), d) && d->params().size() != num_parameters - 1) {
+                    throw default_exception("datatype has already been registered but with a different number of parameters");
+                }
                                 
                 sort* s = m_manager->mk_sort(name.get_symbol(),
                                              sort_info(m_family_id, k, num_parameters, parameters, true));
-                def* d = nullptr;
                 if (m_defs.find(s->get_name(), d) && d->sort_size() && d->params().size() == num_parameters - 1) {
                     obj_map<sort, sort_size> S;
                     for (unsigned i = 0; i + 1 < num_parameters; ++i) {
@@ -345,6 +349,10 @@ namespace datatype {
                 m_manager->raise_exception("invalid datatype");
                 return nullptr;
             }
+            catch (const default_exception & ex) {
+                m_manager->raise_exception(ex.what());
+                return nullptr;
+            }
         }
 
         func_decl * plugin::mk_update_field(