diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index d502aaac9..0d7d50a92 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -17,7 +17,7 @@ z3_add_component(smt
     seq_offset_eq.cpp
     seq_regex.cpp
     seq_skolem.cpp
-    seq_unicode.cpp
+    seq_char.cpp
     smt_almost_cg_table.cpp
     smt_arith_value.cpp
     smt_case_split_queue.cpp
diff --git a/src/smt/seq_unicode.cpp b/src/smt/seq_char.cpp
similarity index 89%
rename from src/smt/seq_unicode.cpp
rename to src/smt/seq_char.cpp
index 2a10369e4..0cce9bf04 100644
--- a/src/smt/seq_unicode.cpp
+++ b/src/smt/seq_char.cpp
@@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation
 
 Module Name:
 
-    seq_unicode.cpp
+    seq_char.cpp
 
 Abstract:
 
-    Solver for unicode characters
+    Solver for characters
 
 Author:
 
@@ -15,26 +15,29 @@ Author:
 
 --*/
 
-#include "smt/seq_unicode.h"
+#include "ast/bv_decl_plugin.h"
+#include "smt/seq_char.h"
 #include "smt/smt_context.h"
 
 namespace smt {
 
-    seq_unicode::seq_unicode(theory& th):
+    seq_char::seq_char(theory& th):
         th(th),
         m(th.get_manager()),
         seq(m),
         m_bb(m, ctx().get_fparams())
     {
-        m_enabled = gparams::get_value("unicode") == "true";
+        bv_util bv(m);
+        sort_ref b8(bv.mk_sort(8), m);
+        m_enabled = seq.is_char(b8);
         m_bits2char = symbol("bits2char");
     }
 
-    struct seq_unicode::reset_bits : public trail<context> {
-        seq_unicode& s;
+    struct seq_char::reset_bits : public trail<context> {
+        seq_char& s;
         unsigned idx;
 
-        reset_bits(seq_unicode& s, unsigned idx):
+        reset_bits(seq_char& s, unsigned idx):
             s(s),
             idx(idx)
         {}
@@ -45,7 +48,7 @@ namespace smt {
         }
     };
 
-    bool seq_unicode::has_bits(theory_var v) const {
+    bool seq_char::has_bits(theory_var v) const {
         return (m_bits.size() > (unsigned)v) && !m_bits[v].empty();
     }
 
@@ -59,7 +62,7 @@ namespace smt {
      * independently and adds Ackerman axioms on demand.
      */
 
-    void seq_unicode::init_bits(theory_var v) {
+    void seq_char::init_bits(theory_var v) {
         if (has_bits(v))
             return;
 
@@ -100,7 +103,7 @@ namespace smt {
         ++m_stats.m_num_blast;
     }
 
-    void seq_unicode::internalize_le(literal lit, app* term) {
+    void seq_char::internalize_le(literal lit, app* term) {
         expr* x = nullptr, *y = nullptr;
         VERIFY(seq.is_char_le(term, x, y));
         theory_var v1 = ctx().get_enode(x)->get_th_var(th.get_id());
@@ -117,18 +120,18 @@ namespace smt {
         ctx().mk_th_axiom(th.get_id(), lit, ~le);
     }
 
-    literal_vector const& seq_unicode::get_bits(theory_var v) {
+    literal_vector const& seq_char::get_bits(theory_var v) {
         init_bits(v);
         return m_bits[v];
     }
 
-    expr_ref_vector const& seq_unicode::get_ebits(theory_var v) {
+    expr_ref_vector const& seq_char::get_ebits(theory_var v) {
         init_bits(v);
         return m_ebits[v];
     }
         
     // = on characters
-    void seq_unicode::new_eq_eh(theory_var v, theory_var w) {  
+    void seq_char::new_eq_eh(theory_var v, theory_var w) {  
         if (has_bits(v) && has_bits(w)) {
             auto& a = get_bits(v);
             auto& b = get_bits(w);            
@@ -160,7 +163,7 @@ namespace smt {
     }
 
     // != on characters
-    void seq_unicode::new_diseq_eh(theory_var v, theory_var w) {  
+    void seq_char::new_diseq_eh(theory_var v, theory_var w) {  
         if (has_bits(v) && has_bits(w)) {
             auto& a = get_bits(v);
             auto& b = get_bits(w);
@@ -174,7 +177,7 @@ namespace smt {
         }
     }
 
-    void seq_unicode::new_const_char(theory_var v, unsigned c) {
+    void seq_char::new_const_char(theory_var v, unsigned c) {
         auto& bits = get_bits(v);
         for (auto b : bits) {
             bool bit = (0 != (c & 1));
@@ -189,7 +192,7 @@ namespace smt {
      *    Enforce that values are within max_char.
      * 2. Assign values to characters that haven't been assigned.
      */
-    bool seq_unicode::final_check() {   
+    bool seq_char::final_check() {   
         m_var2value.reset();
         m_var2value.resize(th.get_num_vars(), UINT_MAX);
         m_value2var.reset();
@@ -251,7 +254,7 @@ namespace smt {
         return true;
     }
 
-    void seq_unicode::enforce_bits() {
+    void seq_char::enforce_bits() {
         TRACE("seq", tout << "enforce bits\n";);
         for (unsigned v = th.get_num_vars(); v-- > 0; ) {
             expr* e = th.get_expr(v);
@@ -260,7 +263,7 @@ namespace smt {
         }        
     }
 
-    void seq_unicode::enforce_value_bound(theory_var v) {
+    void seq_char::enforce_value_bound(theory_var v) {
         TRACE("seq", tout << "enforce bound " << v << "\n";);
         enode* n = th.ensure_enode(seq.mk_char(seq.max_char()));
         theory_var w = n->get_th_var(th.get_id());                    
@@ -274,7 +277,7 @@ namespace smt {
         ++m_stats.m_num_bounds;
     }
 
-    void seq_unicode::enforce_ackerman(theory_var v, theory_var w) {
+    void seq_char::enforce_ackerman(theory_var v, theory_var w) {
         if (v > w) 
             std::swap(v, w);
         TRACE("seq", tout << "enforce ackerman " << v << " " << w << "\n";);
@@ -298,11 +301,11 @@ namespace smt {
         ++m_stats.m_num_ackerman;
     }
     
-    unsigned seq_unicode::get_value(theory_var v) {
+    unsigned seq_char::get_value(theory_var v) {
         return m_var2value[v];
     }
 
-    bool seq_unicode::get_value(theory_var v, unsigned& c) {
+    bool seq_char::get_value(theory_var v, unsigned& c) {
         if (!has_bits(v))
             return false;
         auto const & b = get_bits(v);
@@ -316,7 +319,7 @@ namespace smt {
         return true;
     }
 
-    void seq_unicode::collect_statistics(::statistics& st) const {
+    void seq_char::collect_statistics(::statistics& st) const {
         st.update("seq char ackerman", m_stats.m_num_ackerman);
         st.update("seq char bounds",   m_stats.m_num_bounds);
         st.update("seq char2bit",      m_stats.m_num_blast);
diff --git a/src/smt/seq_unicode.h b/src/smt/seq_char.h
similarity index 95%
rename from src/smt/seq_unicode.h
rename to src/smt/seq_char.h
index c81803253..fe28989cf 100644
--- a/src/smt/seq_unicode.h
+++ b/src/smt/seq_char.h
@@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation
 
 Module Name:
 
-    seq_unicode.h
+    seq_char.h
 
 Abstract:
 
-    Solver for unicode characters
+    Solver for characters
 
 Author:
 
@@ -23,7 +23,7 @@ Author:
 
 namespace smt {
 
-    class seq_unicode {
+    class seq_char {
 
 
         struct stats {
@@ -68,7 +68,7 @@ namespace smt {
 
     public:
 
-        seq_unicode(theory& th);
+        seq_char(theory& th);
 
         bool enabled() const { return m_enabled; }
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4db358431..6920a63a3 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -272,7 +272,7 @@ theory_seq::theory_seq(context& ctx):
     m_autil(m),
     m_sk(m, m_rewrite),
     m_ax(*this, m_rewrite),
-    m_unicode(*this),
+    m_char(*this),
     m_regex(*this),
     m_arith_value(m),
     m_trail_stack(*this),
@@ -354,7 +354,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("zero_length");
         return FC_CONTINUE;
     }
-    if (m_unicode.enabled() && !m_unicode.final_check()) {
+    if (m_char.enabled() && !m_char.final_check()) {
         return FC_CONTINUE;
     }
     if (get_fparams().m_split_w_len && len_based_split()) {
@@ -1489,10 +1489,10 @@ bool theory_seq::internalize_term(app* term) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());
         ctx.mark_as_relevant(bv);
-        if (m_util.is_char_le(term) && m_unicode.enabled()) {
+        if (m_util.is_char_le(term) && m_char.enabled()) {
             mk_var(ensure_enode(term->get_arg(0)));
             mk_var(ensure_enode(term->get_arg(1)));
-            m_unicode.internalize_le(literal(bv, false), term);
+            m_char.internalize_le(literal(bv, false), term);
         }
     }
 
@@ -1509,8 +1509,8 @@ bool theory_seq::internalize_term(app* term) {
     }
 
     unsigned c = 0;
-    if (m_unicode.enabled() && m_util.is_const_char(term, c))
-        m_unicode.new_const_char(v, c);
+    if (m_char.enabled() && m_util.is_const_char(term, c))
+        m_char.new_const_char(v, c);
     
     return true;
 }
@@ -1769,7 +1769,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq extensionality", m_stats.m_extensionality);
     st.update("seq fixed length", m_stats.m_fixed_length);
     st.update("seq int.to.str", m_stats.m_int_string);
-    m_unicode.collect_statistics(st);
+    m_char.collect_statistics(st);
 }
 
 void theory_seq::init_search_eh() {
@@ -1992,8 +1992,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
         m_concat.shrink(start);        
         return sv;
     }
-    else if (m_unicode.enabled() && m_util.is_char(e)) {
-        unsigned ch = m_unicode.get_value(n->get_th_var(get_id()));
+    else if (m_char.enabled() && m_util.is_char(e)) {
+        unsigned ch = m_char.get_value(n->get_th_var(get_id()));
         app* val = m_util.str.mk_char(ch);
         m_factory->add_trail(val);
         return alloc(expr_wrapper_proc, val);
@@ -2302,7 +2302,7 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
 theory_var theory_seq::mk_var(enode* n) {
     expr* o = n->get_owner();
 
-    if (!m_util.is_seq(o) && !m_util.is_re(o) && (!m_unicode.enabled() || !m_util.is_char(o)))
+    if (!m_util.is_seq(o) && !m_util.is_re(o) && (!m_char.enabled() || !m_util.is_char(o)))
         return null_theory_var;
 
     if (is_attached_to_var(n)) 
@@ -2961,7 +2961,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
         // no-op
     }
-    else if (m_unicode.enabled() && m_util.is_char_le(e)) {
+    else if (m_char.enabled() && m_util.is_char_le(e)) {
         // no-op
     }
     else if (m_util.is_skolem(e)) {
@@ -2982,8 +2982,8 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
     enode* n2 = get_enode(v2);
     expr* o1 = n1->get_owner();
     expr* o2 = n2->get_owner();
-    if (m_unicode.enabled() && m_util.is_char(o1)) {
-        m_unicode.new_eq_eh(v1, v2);
+    if (m_char.enabled() && m_util.is_char(o1)) {
+        m_char.new_eq_eh(v1, v2);
         return;
     }
     if (!m_util.is_seq(o1) && !m_util.is_re(o1))
@@ -3033,8 +3033,8 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
         m_regex.propagate_ne(e1, e2);
         return;
     }
-    if (m_unicode.enabled() && m_util.is_char(n1->get_owner())) {
-        m_unicode.new_diseq_eh(v1, v2);
+    if (m_char.enabled() && m_util.is_char(n1->get_owner())) {
+        m_char.new_diseq_eh(v1, v2);
         return;
     }
     if (!m_util.is_seq(e1))
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f98eaf9cf..0c1108ce4 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -31,7 +31,7 @@ Revision History:
 #include "smt/theory_seq_empty.h"
 #include "smt/seq_skolem.h"
 #include "smt/seq_axioms.h"
-#include "smt/seq_unicode.h"
+#include "smt/seq_char.h"
 #include "smt/seq_regex.h"
 #include "smt/seq_offset_eq.h"
 
@@ -356,7 +356,7 @@ namespace smt {
         arith_util       m_autil;
         seq_skolem       m_sk;
         seq_axioms       m_ax;
-        seq_unicode      m_unicode;
+        seq_char         m_char;
         seq_regex        m_regex;
         arith_value      m_arith_value;
         th_trail_stack   m_trail_stack;