diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index a2a0e1da0..41f3a6b50 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1037,8 +1037,8 @@ app* seq_decl_plugin::mk_char(unsigned u) {
         return m_manager->mk_const(f);
     }
     else {
-        UNREACHABLE();
-        return nullptr;
+        bv_util bv(*m_manager);
+        return bv.mk_numeral(rational(u), 8);
     }
 }
 
@@ -1124,6 +1124,7 @@ expr* seq_decl_plugin::get_some_value(sort* s) {
     return nullptr;
 }
 
+
 app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
     SASSERT(range);    
     parameter param(name);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 39fbb1fc6..5729b4ab9 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -238,6 +238,9 @@ public:
     bool has_seq() const { return m_has_seq; }
 
     bool is_considered_uninterpreted(func_decl * f) override;
+
+    sort* char_sort() const { return m_char; }
+    sort* string_sort() const { return m_string; }
 };
 
 class seq_util {
@@ -254,6 +257,9 @@ public:
 
     ast_manager& get_manager() const { return m; }
 
+    sort* mk_char_sort() const { return seq.char_sort(); }
+    sort* mk_string_sort() const { return seq.string_sort(); }
+
     bool is_char(sort* s) const { return seq.is_char(s); }
     bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp
index c8a6f3dcb..afb134d38 100644
--- a/src/smt/theory_str_mc.cpp
+++ b/src/smt/theory_str_mc.cpp
@@ -619,9 +619,6 @@ namespace smt {
 
         ast_manager & sub_m = subsolver.m();
 
-        bv_util bv(m);
-        sort * bv8_sort = bv.mk_sort(8);
-
         expr * arg0;
         expr * arg1;
         expr * arg2;
@@ -646,7 +643,7 @@ namespace smt {
                 ptr_vector<expr> new_chars;
                 for (rational i = rational::zero(); i < varLen_value; ++i) {
                     // TODO we can probably name these better for the sake of debugging
-                    expr_ref ch(mk_fresh_const("char", bv8_sort), m);
+                    expr_ref ch(mk_fresh_const("char", u.mk_char_sort()), m);
                     new_chars.push_back(ch);
                     fixed_length_subterm_trail.push_back(ch);
                 }
@@ -791,7 +788,7 @@ namespace smt {
                 TRACE("str_fl", tout << "creating character terms for uninterpreted function " << mk_pp(term, m) << ", length = " << ufLen_value << std::endl;);
                 ptr_vector<expr> new_chars;
                 for (rational i = rational::zero(); i < ufLen_value; ++i) {
-                    expr_ref ch(mk_fresh_const("char", bv8_sort), m);
+                    expr_ref ch(mk_fresh_const("char", u.mk_char_sort()), m);
                     new_chars.push_back(ch);
                     fixed_length_subterm_trail.push_back(ch);
                 }
@@ -888,11 +885,8 @@ namespace smt {
         ast_manager & m = get_manager();
 
         if (bitvector_character_constants.empty()) {
-            bv_util bv(m);
-            sort * bv8_sort = bv.mk_sort(8);
-            for (unsigned i = 0; i < 256; ++i) {
-                rational ch(i);
-                expr_ref chTerm(bv.mk_numeral(ch, bv8_sort), m);
+            for (unsigned i = 0; i <= u.max_char(); ++i) {
+                expr_ref chTerm(u.mk_char(i), m);
                 bitvector_character_constants.push_back(chTerm);
                 fixed_length_subterm_trail.push_back(chTerm);
             }
@@ -1232,7 +1226,6 @@ namespace smt {
         lbool subproblem_status = subsolver.check(fixed_length_assumptions);
 
         if (subproblem_status == l_true) {
-            bv_util bv(m);
             TRACE("str_fl", tout << "subsolver found SAT; reconstructing model" << std::endl;);
             model_ref subModel;
             subsolver.get_model(subModel);
@@ -1246,9 +1239,9 @@ namespace smt {
                 ptr_vector<expr> char_subterms(entry.m_value);
                 for (expr * chExpr : char_subterms) {
                     expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
-                    rational n;
-                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
-                        assignment.push_back(n.get_unsigned());
+                    unsigned n = 0;
+                    if (chAssignment != nullptr && u.is_const_char(chAssignment, n)) {
+                        assignment.push_back(n);
                     } else {
                         assignment.push_back((unsigned)'?');
                     }
@@ -1268,9 +1261,9 @@ namespace smt {
                 ptr_vector<expr> char_subterms(entry.m_value);
                 for (expr * chExpr : char_subterms) {
                     expr_ref chAssignment(subModel->get_const_interp(to_app(chExpr)->get_decl()), m);
-                    rational n;
-                    if (chAssignment != nullptr && bv.is_numeral(chAssignment, n) && n.is_unsigned()) {
-                        assignment.push_back(n.get_unsigned());
+                    unsigned n = 0;
+                    if (chAssignment != nullptr && u.is_const_char(chAssignment, n)) {
+                        assignment.push_back(n);
                     } else {
                         assignment.push_back((unsigned)'?');
                     }