diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 3ad20cf90..650afda25 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -63,6 +63,7 @@ void smt_params::updt_params(params_ref const & p) {
     theory_bv_params::updt_params(p);
     theory_pb_params::updt_params(p);
     // theory_array_params::updt_params(p);
+    theory_datatype_params::updt_params(p);
     updt_local_params(p);
 }
 
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 3f4105c34..76e9f03b1 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -94,5 +94,6 @@ def_module_params(module_name='smt',
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
                           ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
-                          ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none')
+                          ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
+                          ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
                           ))
diff --git a/src/smt/params/theory_datatype_params.h b/src/smt/params/theory_datatype_params.h
index 9f801e46c..d2d851ffe 100644
--- a/src/smt/params/theory_datatype_params.h
+++ b/src/smt/params/theory_datatype_params.h
@@ -19,6 +19,8 @@ Revision History:
 #ifndef THEORY_DATATYPE_PARAMS_H_
 #define THEORY_DATATYPE_PARAMS_H_
 
+#include "smt/params/smt_params_helper.hpp"
+
 struct theory_datatype_params {
     unsigned   m_dt_lazy_splits;
 
@@ -26,11 +28,10 @@ struct theory_datatype_params {
         m_dt_lazy_splits(1) {
     }
 
-#if 0
-    void register_params(ini_params & p) {
-        p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy");
+    void updt_params(params_ref const & _p) {
+        smt_params_helper p(_p);
+        m_dt_lazy_splits = p.dt_lazy_splits(); 
     }
-#endif
 
     void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
 };