diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b67163f7c..bbb225387 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -45,14 +45,13 @@ expr_ref sym_expr::accept(expr* e) {
         result = m.mk_eq(e, m_t);
         break;
     case t_range: {
-        bv_util bv(m);
-        rational r1, r2, r3;
-        unsigned sz;
-        if (bv.is_numeral(m_t, r1, sz) && bv.is_numeral(e, r2, sz) && bv.is_numeral(m_s, r3, sz)) {
+        seq_util u(m);
+        unsigned r1, r2, r3;
+        if (u.is_const_char(m_t, r1) && u.is_const_char(e, r2) && u.is_const_char(m_s, r3)) {
             result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));            
         }
         else {
-            result = m.mk_and(bv.mk_ule(m_t, e), bv.mk_ule(e, m_s));
+            result = m.mk_and(u.mk_le(m_t, e), u.mk_le(e, m_s));
         }
         break;
     }
@@ -190,7 +189,7 @@ public:
     }*/
 };
 
-re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(nullptr), m_sa(nullptr) {}
+re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
 
 re2automaton::~re2automaton() {}
 
@@ -248,9 +247,8 @@ eautomaton* re2automaton::re2aut(expr* e) {
             s1.length() == 1 && s2.length() == 1) {
             unsigned start = s1[0];
             unsigned stop = s2[0];
-            unsigned nb = s1.num_bits();
-            expr_ref _start(bv.mk_numeral(start, nb), m);
-            expr_ref _stop(bv.mk_numeral(stop, nb), m);
+            expr_ref _start(u.mk_char(start), m);
+            expr_ref _stop(u.mk_char(stop), m);
             TRACE("seq", tout << "Range: " << start << " " << stop << "\n";);
             a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
             return a.detach();
@@ -463,14 +461,12 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
  * (seq.unit (_ BitVector 8)) ==> String constant
  */
 br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
-    bv_util bvu(m());
-    rational n_val;
-    unsigned int n_size;
+    unsigned ch;
     // specifically we want (_ BitVector 8)
-    if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
+    if (m_util.is_const_char(e, ch)) {
         // convert to string constant
-        zstring str(n_val.get_unsigned());
-        TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
+        zstring str(ch);
+        TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << ch << " to string constant \"" << str<< "\"" << std::endl;);
         result = m_util.str.mk_string(str);
         return BR_DONE;
     }
@@ -1977,15 +1973,13 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) {
 bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
     zstring s1;
     expr* e;
-    bv_util bv(m());
-    rational val;
-    unsigned sz;
+    unsigned ch;
     for (unsigned i = 0; i < n; ++i) {
         if (m_util.str.is_string(es[i], s1)) {
             s = s + s1;
         }
-        else if (m_util.str.is_unit(es[i], e) && bv.is_numeral(e, val, sz)) {
-            s = s + zstring(val.get_unsigned());
+        else if (m_util.str.is_unit(es[i], e) && m_util.is_const_char(e, ch)) {
+            s = s + zstring(ch);
         }
         else {
             return false;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index f5878b2c2..c2b2227b2 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -77,7 +77,6 @@ class re2automaton {
     ast_manager& m;
     sym_expr_manager sm;
     seq_util     u;     
-    bv_util      bv;
     scoped_ptr<expr_solver>         m_solver;
     scoped_ptr<boolean_algebra_t>   m_ba;
     scoped_ptr<symbolic_automata_t> m_sa;
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 0bfc94e11..2210fc04b 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "ast/arith_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "ast/bv_decl_plugin.h"
 #include <sstream>
 
 static bool is_hex_digit(char ch, unsigned& d) {
@@ -967,6 +968,24 @@ app*  seq_util::str::mk_char(char ch) const {
     return mk_char(s, 0);
 }
 
+bool seq_util::is_const_char(expr* e, unsigned& c) const {
+    bv_util bv(m);
+    rational r;    
+    unsigned sz;
+    return bv.is_numeral(e, r, sz) && r.is_unsigned(), c = r.get_unsigned(), true;
+}
+
+app* seq_util::mk_char(unsigned ch) const {
+    bv_util bv(m);
+    return bv.mk_numeral(rational(ch), 8);
+}
+
+app* seq_util::mk_le(expr* ch1, expr* ch2) const {
+    bv_util bv(m);
+    return bv.mk_ule(ch1, ch2);
+}
+
+
 bool seq_util::str::is_string(expr const* n, zstring& s) const {
     if (is_string(n)) {
         s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 4b23f81d0..1148c8411 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -22,7 +22,6 @@ Revision History:
 #define SEQ_DECL_PLUGIN_H_
 
 #include "ast/ast.h"
-#include "ast/bv_decl_plugin.h"
 
 
 enum seq_sort_kind {
@@ -221,6 +220,9 @@ public:
     bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
     bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
     bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
+    bool is_const_char(expr* e, unsigned& c) const;
+    app* mk_char(unsigned ch) const;
+    app* mk_le(expr* ch1, expr* ch2) const;
 
     app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
     bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d418bd437..5d1ec835b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1573,7 +1573,6 @@ namespace opt {
                            m_model_converter->display(verbose_stream() << "mc\n");
                            model_smt2_pp(verbose_stream(), m, *mdl, 0);
                            verbose_stream() << to_string_internal() << "\n");
-                exit(0);
             }
         }
     }
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index 9054e2b00..17c3f9128 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -403,10 +403,8 @@ namespace smt {
                 }
                 int new_break_count = flip(~lit);
                 if (-break_count != new_break_count) {
-                    verbose_stream() << lit << "\n";
-                    IF_VERBOSE(0, display(verbose_stream(), cls););
-                    display(verbose_stream());
-                    exit(0);
+                    IF_VERBOSE(0, display(verbose_stream() << lit << "\n", cls);
+                               display(verbose_stream()));
                 }
                 // VERIFY(-break_count == flip(~lit));
             }            
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 762939b74..b1502d98e 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -676,7 +676,6 @@ namespace sat {
                 verbose_stream() << "alit: " << alit << "\n";
                 verbose_stream() << "num watch " << num_watch << "\n");
             UNREACHABLE();
-            exit(0);
             return l_undef;
         }
         
@@ -2606,7 +2605,6 @@ namespace sat {
                 IF_VERBOSE(0, s().display_watches(verbose_stream()));
 
                 UNREACHABLE();
-                exit(1);
                 return false;
             }
         }
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 932e9b35e..529a6bc57 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -288,7 +288,6 @@ namespace sat {
                   display(tout); 
                   s.display(tout););
             UNREACHABLE();
-            exit(0);
         }
     }
 
diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index d132f1cd4..17885f4e5 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -95,7 +95,7 @@ namespace sat {
                         IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n");
                         IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";);
                         IF_VERBOSE(0, display(verbose_stream()));
-                        exit(0);
+                        UNREACHABLE();
                         first = false;
                     }
                     if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {     
diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp
index 50fe6340a..8dfca3ebb 100644
--- a/src/smt/smt_arith_value.cpp
+++ b/src/smt/smt_arith_value.cpp
@@ -92,8 +92,18 @@ namespace smt {
         return false;
     }
 
+    bool arith_value::get_value(expr* e, rational& val) const {
+        if (!m_ctx->e_internalized(e)) return false;
+        expr_ref _val(m);
+        enode* n = m_ctx->get_enode(e);
+        if (m_tha && m_tha->get_value(n, _val) && a.is_numeral(_val, val)) return true;
+        if (m_thi && m_thi->get_value(n, _val) && a.is_numeral(_val, val)) return true;
+        if (m_thr && m_thr->get_value(n, val)) return true;
+        return false;
+    }
 
-    bool arith_value::get_value(expr* e, rational& val) {
+
+    bool arith_value::get_value_equiv(expr* e, rational& val) const {
         if (!m_ctx->e_internalized(e)) return false;
         expr_ref _val(m);
         enode* next = m_ctx->get_enode(e), *n = next;
diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h
index ddaa113ea..7fa1ecc31 100644
--- a/src/smt/smt_arith_value.h
+++ b/src/smt/smt_arith_value.h
@@ -38,9 +38,10 @@ namespace smt {
         void init(context* ctx);
         bool get_lo_equiv(expr* e, rational& lo, bool& strict);
         bool get_up_equiv(expr* e, rational& up, bool& strict);
-        bool get_value(expr* e, rational& value);
+        bool get_value_equiv(expr* e, rational& value) const;
         bool get_lo(expr* e, rational& lo, bool& strict) const;
         bool get_up(expr* e, rational& up, bool& strict) const;
+        bool get_value(expr* e, rational& value) const;
         bool get_fixed(expr* e, rational& value) const;
         final_check_status final_check();
     };
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 33207d15a..2cc88b901 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include "smt/theory_bv.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/bv_decl_plugin.h"
 #include "smt/smt_model_generator.h"
 #include "util/stats.h"
 
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 152eb715b..1499c102d 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -576,7 +576,7 @@ namespace smt {
         arith_value av(get_manager());
         av.init(&get_context());
         rational val;
-        if (av.get_value(e, val) && val.is_uint64()) {
+        if (av.get_value_equiv(e, val) && val.is_uint64()) {
             return val.get_uint64();
         }
         return 0;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 4ff0fb7bc..298502fe8 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3457,9 +3457,8 @@ void theory_seq::add_itos_axiom(expr* e) {
 void theory_seq::ensure_digit_axiom() {
 
     if (m_si_axioms.empty()) {
-        bv_util bv(m);
         for (unsigned i = 0; i < 10; ++i) {
-            expr_ref cnst(bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), m);
+            expr_ref cnst(m_util.mk_char('0'+i), m);
             add_axiom(mk_eq(digit2int(cnst), m_autil.mk_int(i), false));
         }
     }
@@ -3512,11 +3511,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
 }
 
 literal theory_seq::is_digit(expr* ch) {
-    bv_util bv(m);
     literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()));
     expr_ref d2i = digit2int(ch);
-    expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
-    expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
+    expr_ref _lo(m_util.mk_le(m_util.mk_char('0'), ch), m);
+    expr_ref _hi(m_util.mk_le(ch, m_util.mk_char('9')), m);
     literal lo = mk_literal(_lo);
     literal hi = mk_literal(_hi);
     add_axiom(~lo, ~hi, isd);
@@ -3817,18 +3815,17 @@ public:
         SASSERT(values.size() == m_dependencies.size());
         expr_ref_vector args(th.m);
         unsigned j = 0, k = 0;
+        rational val;
         bool is_string = th.m_util.is_string(m_sort);
         expr_ref result(th.m);
         if (is_string) {
             unsigned_vector sbuffer;
-            bv_util bv(th.m);
-            rational val;
-            unsigned sz;
+            unsigned ch;
             for (source_t src : m_source) {
                 switch (src) {
                 case unit_source: {
-                    VERIFY(bv.is_numeral(values[j++], val, sz));
-                    sbuffer.push_back(val.get_unsigned());
+                    VERIFY(th.m_util.is_const_char(values[j++], ch));
+                    sbuffer.push_back(ch);
                     break;
                 }
                 case string_source: {
@@ -4634,32 +4631,9 @@ static T* get_th_arith(context& ctx, theory_id afid, expr* e) {
     }
 }
 
-static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v) {
-    theory_mi_arith* tha = get_th_arith<theory_mi_arith>(ctx, afid, e);
-    if (tha) return tha->get_value(ctx.get_enode(e), v);
-    theory_i_arith* thi = get_th_arith<theory_i_arith>(ctx, afid, e);
-    if (thi) return thi->get_value(ctx.get_enode(e), v);
-    theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
-    if (thr) return thr->get_value(ctx.get_enode(e), v);
-    TRACE("seq", tout << "no arithmetic theory\n";);
-    return false;
-}
 
 bool theory_seq::get_num_value(expr* e, rational& val) const {
-    context& ctx = get_context();
-    expr_ref _val(m);
-    if (!ctx.e_internalized(e))
-        return false;
-    enode* next = ctx.get_enode(e), *n = next;
-    do { 
-        if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
-            return true;
-        }
-        next = next->get_next();
-    }
-    while (next != n);
-    TRACE("seq", tout << "no value for " << mk_pp(e, m) << "\n";);
-    return false;
+    return m_arith_value.get_value_equiv(e, val) && val.is_int();
 }
 
 bool theory_seq::lower_bound(expr* e, rational& lo) const {
@@ -4748,9 +4722,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
         }
         else {            
             len = mk_len(c);
-            if (ctx.e_internalized(len) &&
-                get_arith_value(ctx, m_autil.get_family_id(), len, len_val) &&
-                m_autil.is_numeral(len_val, val1)) {
+            if (m_arith_value.get_value(len, val1)) {
                 val += val1;
             }
             else {
@@ -5050,13 +5022,14 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
 
-expr* theory_seq::coalesce_chars(expr* const& e) {
+expr_ref theory_seq::coalesce_chars(expr* const& e) {
     context& ctx = get_context();
     expr* s;
+    unsigned ch;
+    expr_ref result(m);
     if (m_util.str.is_concat(e)) {
-        expr_ref_vector concats(m);
+        expr_ref_vector rs(m), concats(m);
         m_util.str.get_concat(e, concats);
-        expr_ref_vector result(m);
         for (unsigned i = 0; i < concats.size(); ++i) {
             expr_ref tmp(coalesce_chars(concats[i].get()), m);
             if (m_util.str.is_empty(tmp)) continue;
@@ -5076,32 +5049,30 @@ expr* theory_seq::coalesce_chars(expr* const& e) {
                 }
             }
             if (flag) {
-                result.push_back(m_util.str.mk_string(zs));
+                rs.push_back(m_util.str.mk_string(zs));
                 if (i < concats.size())
-                    result.push_back(tmp);
+                    rs.push_back(tmp);
             }
             else
-                result.push_back(tmp);
+                rs.push_back(tmp);
         }
-        SASSERT(result.size() > 0);
-        if (result.size() > 1)
-            return m_util.str.mk_concat(result.size(), result.c_ptr());
-        else 
-            return e;
-    }
-    else if (m_util.str.is_unit(e, s)) {
-        bv_util bvu(m);
-        if (bvu.is_bv(s)) {
-            expr_ref result(m);
-            expr * args[1] = {s};
-            if (BR_FAILED != m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, args, result)) {
-                if (!ctx.e_internalized(result))
-                    ctx.internalize(result, false);
-                return result;
-            }
+        SASSERT(rs.size() > 0);
+        if (rs.size() > 1) {
+            return expr_ref(m_util.str.mk_concat(rs.size(), rs.c_ptr()), m);
+        }
+        else {
+            result = e;
+            return result;
         }
     }
-    return e;
+    else if (m_util.str.is_unit(e, s) && m_util.is_const_char(s, ch) &&
+             BR_FAILED != m_seq_rewrite.mk_app_core(to_app(e)->get_decl(), 1, &s, result)) {
+        if (!ctx.e_internalized(result))
+            ctx.internalize(result, false);
+        return result;
+    }
+    result = e;
+    return result;
 }
 
 expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) {
@@ -5111,9 +5082,11 @@ expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3,
     if (!range) {
         range = m.get_sort(e1);
     }
+    expr_ref_vector pinned(m);        
     if (name == m_seq_align) {
         for (unsigned i = 0; i < len; ++i) {
-            es[i] = coalesce_chars(es[i]);
+            pinned.push_back(coalesce_chars(es[i]));
+            es[i] = pinned.back();
             TRACE("seq", tout << mk_pp(es[i], m) << "\n";);
         }
     }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 9df28acf5..929626757 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -606,7 +606,7 @@ namespace smt {
         bool get_length(expr* s, rational& val) const;
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
-        expr* coalesce_chars(expr* const& str);
+        expr_ref coalesce_chars(expr* const& str);
         expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr);
         bool is_skolem(symbol const& s, expr* e) const;
 
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 0e2128990..fc6ec6f7a 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -209,7 +209,6 @@ void solver::assert_expr(expr* f, expr* t) {
     expr_ref a(t, m);
     if (m_enforce_model_conversion) {
         IF_VERBOSE(0, verbose_stream() << "enforce model conversion\n";);
-        exit(0);
         model_converter_ref mc = get_model_converter();
         if (mc) {
             (*mc)(fml);