diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 6ad306d2d..0c690f3f5 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -26,7 +26,6 @@ Revision History:
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false),
                                     m_stringc_sym("String"),
-                                    m_charc_sym("Char"),
                                     m_string(nullptr),
                                     m_char(nullptr),
                                     m_reglan(nullptr),
@@ -1408,8 +1407,8 @@ seq_util::rex::info seq_util::rex::info::plus() const {
 }
 
 seq_util::rex::info seq_util::rex::info::opt() const {
-    //if is_known() is false then all mentioned properties will remain false
-    //optional construct never occurs in a normalized regex
+    // if is_known() is false then all mentioned properties will remain false
+    // optional construct never occurs in a normalized regex
     return seq_util::rex::info(classical, classical, interpreted, nonbranching, false, monadic, false, l_true, 0, star_height);
 }
 
@@ -1512,7 +1511,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
         if (i.is_known()) {
             // unsigned ite_min_length = std::min(min_length, i.min_length);
             // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef);
-            //TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
+            // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
             return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height));
         }
         else
@@ -1529,16 +1528,16 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) co
             m = UINT_MAX;
         lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
         if (upper == UINT_MAX) {
-            //this means the loop is r{lower,*} and is therefore not normalized
-            //normalized regex would be r{lower,lower}r* and would in particular not use r{0,} for r*
+            // this means the loop is r{lower,*} and is therefore not normalized
+            // normalized regex would be r{lower,lower}r* and would in particular not use r{0,} for r*
             return info(classical, classical, interpreted, nonbranching, false, singleton, false, loop_nullable, m, star_height + 1);
         }
         else {
             bool loop_normalized = normalized;
-            //r{lower,upper} is not normalized if r is nullable but lower > 0
-            //r{0,1} is not normalized: it should be ()|r
-            //r{1,1} is not normalized: it should be r
-            //r{lower,upper} is not normalized if lower > upper it should then be [] (empty)
+            // r{lower,upper} is not normalized if r is nullable but lower > 0
+            // r{0,1} is not normalized: it should be ()|r
+            // r{1,1} is not normalized: it should be r
+            // r{lower,upper} is not normalized if lower > upper it should then be [] (empty)
             if ((nullable == l_true && lower > 0) || upper == 1 || lower > upper)
                 loop_normalized = false;
             return info(classical, classical, interpreted, nonbranching, loop_normalized, singleton, false, loop_nullable, m, star_height);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index ef5049476..5a12677b2 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -128,7 +128,6 @@ class seq_decl_plugin : public decl_plugin {
     ptr_vector<sort> m_binding;
     bool             m_init;
     symbol           m_stringc_sym;
-    symbol           m_charc_sym;
     sort*            m_string;
     sort*            m_char;
     sort*            m_reglan;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index bccc840fc..0d683b1ff 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -934,14 +934,7 @@ namespace smt {
     }
 
     void setup::setup_char() {
-        // temporary: enable only char theory if it is used in seq
-        seq_util seq(m_manager);
-        sort* ch = seq.mk_char_sort();
-        sort* s  = seq.mk_string_sort();
-        family_id ch_fid = ch->get_family_id();
-        if (s->get_family_id() != ch_fid)
-            m_context.register_plugin(alloc(smt::theory_char, m_context, ch_fid));
-        
+        m_context.register_plugin(alloc(smt::theory_char, m_context));        
     }
 
     void setup::setup_special_relations() {
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index 715cb90c6..ab4be4137 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -22,8 +22,8 @@ Author:
 
 namespace smt {
     
-    theory_char::theory_char(context& ctx, family_id fid):
-        theory(ctx, fid),
+    theory_char::theory_char(context& ctx):
+        theory(ctx, ctx.get_manager().mk_family_id("char")),
         seq(m),
         m_bb(m, ctx.get_fparams())
     {
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index 90a403829..c1092f20d 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -64,11 +64,11 @@ namespace smt {
 
     public:
 
-        theory_char(context& ctx, family_id fid);
+        theory_char(context& ctx);
         
         void new_eq_eh(theory_var v1, theory_var v2) override;
         void new_diseq_eh(theory_var v1, theory_var v2) override;
-        theory * mk_fresh(context * new_ctx) override { return alloc(theory_char, *new_ctx, get_family_id()); }
+        theory * mk_fresh(context * new_ctx) override { return alloc(theory_char, *new_ctx); }
         bool internalize_atom(app * atom, bool gate_ctx) override;
         bool internalize_term(app * term) override;
         void display(std::ostream& out) const override {}