diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 7d59225df..4f265eb79 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -242,14 +242,6 @@ namespace sls {
                         args.push_back(m.mk_app(a, t));
                     m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args))));
                 }
-
-                //
-                // sort_size sz = dt.et_datatype_size(s);
-                // if (sz.is_finite()) {
-                //     - sz.size()
-                //     - enumerate instances and set t to be one of instances?
-                // }
-                // 
             }
         }
         collect_path_axioms();
@@ -464,6 +456,15 @@ namespace sls {
                 }
             }                    
         }
+
+
+        //
+        // sort_size sz = dt.et_datatype_size(s);
+        // if (sz.is_finite()) 
+        //     - sz.size() < |T of sort s|
+        //     - ensure that there are at most sz.size() distinct elements.
+        //     - not distinct(t1, ..., tn) where n = sz.size() + 1        
+        // 
         return false;
     }
 
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 362907e46..ce2f3402e 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -39,6 +39,7 @@ Revision History:
 #include "model/datatype_factory.h"
 #include "model/numeral_factory.h"
 #include "model/fpa_factory.h"
+#include "model/char_factory.h"
 
 
 model::model(ast_manager & m):
@@ -103,12 +104,14 @@ value_factory* model::get_factory(sort* s) {
     if (m_factories.plugins().empty()) {
         seq_util su(m);
         fpa_util fu(m);
+        m_factories.register_plugin(alloc(basic_factory, m, 0));
         m_factories.register_plugin(alloc(array_factory, m, *this));
         m_factories.register_plugin(alloc(datatype_factory, m, *this));
         m_factories.register_plugin(alloc(bv_factory, m));
         m_factories.register_plugin(alloc(arith_factory, m));
         m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
         m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id()));
+        //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id());
     }
     family_id fid = s->get_family_id();
     return m_factories.get_plugin(fid);