diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d8afe0b49..6cb95011f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -553,6 +553,9 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
         }
         else if(m_util.str.is_unit(l, a) &&
                 m_util.str.is_unit(r, b)) {
+            if (m.are_distinct(a, b)) {
+                return false;
+            }
             lhs.push_back(a);
             rhs.push_back(b);
             m_lhs.pop_back();
@@ -561,11 +564,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
         else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
             SASSERT(s.length() > 0);
             
-            unsigned ch = s[s.length()-1];
-            SASSERT(s.num_bits() == m_butil.get_bv_size(a));
-            expr_ref bv(m());
-            
-            bv = m_butil.mk_numeral(ch, s.num_bits());
+            expr_ref bv = m_util.str.mk_char(s, s.length()-1);
             SASSERT(m_butil.is_bv(a));
             lhs.push_back(bv);
             rhs.push_back(a);
@@ -611,6 +610,9 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
         }
         else if(m_util.str.is_unit(l, a) &&
                 m_util.str.is_unit(r, b)) {
+            if (m.are_distinct(a, b)) {
+                return false;
+            }
             lhs.push_back(a);
             rhs.push_back(b);
             ++head1;
@@ -618,12 +620,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
         }
         else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) {
             SASSERT(s.length() > 0);
-            
-            unsigned ch = s[0];
-            SASSERT(s.num_bits() == m_butil.get_bv_size(a));
-            expr_ref bv(m());
-            
-            bv = m_butil.mk_numeral(ch, s.num_bits());
+            expr_ref bv = m_util.str.mk_unit(s, 0);
             SASSERT(m_butil.is_bv(a));
             lhs.push_back(bv);
             rhs.push_back(a);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index e33da18f2..14948fdd0 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -124,7 +124,7 @@ bool zstring::contains(zstring const& other) const {
 
 int zstring::indexof(zstring const& other, int offset) const {
     SASSERT(offset >= 0);
-    if (offset == length()) return -1;
+    if (static_cast<unsigned>(offset) == length()) return -1;
     if (other.length() + offset > length()) return -1;
     unsigned last = length() - other.length();
     for (unsigned i = static_cast<unsigned>(offset); i <= last; ++i) {
@@ -312,18 +312,14 @@ void seq_decl_plugin::init() {
     sort* boolT = m.mk_bool_sort();
     sort* intT  = arith_util(m).mk_int();
     sort* predA = array_util(m).mk_array_sort(A, boolT);
-    sort* u16T = 0;
-    sort* u32T = 0;
     sort* seqAseqA[2] = { seqA, seqA };
     sort* seqAreA[2] = { seqA, reA };
     sort* reAreA[2] = { reA, reA };
-    sort* AA[2] = { A, A };
     sort* seqAint2T[3] = { seqA, intT, intT };
     sort* seq2AintT[3] = { seqA, seqA, intT };
     sort* str2T[2] = { strT, strT };
     sort* str3T[3] = { strT, strT, strT };
     sort* strTint2T[3] = { strT, intT, intT };
-    sort* re2T[2] = { reT, reT };
     sort* strTreT[2] = { strT, reT };
     sort* str2TintT[3] = { strT, strT, intT };
     sort* seqAintT[2] = { seqA, intT };
@@ -612,6 +608,14 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
 
 app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); }
 
+
+expr_ref seq_util::str::mk_char(zstring const& s, unsigned idx) {
+    bv_util bvu(m());
+    unsigned ch = s[idx];
+    return expr_ref(bvu.mk_numeral(ch, s.num_bits()), m());
+}
+
+
 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 ce63f8dc8..0db6b55b2 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -207,6 +207,7 @@ public:
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
         app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
 
+        expr_ref mk_unit_char(zstring const& s, unsigned idx);
 
     public:
         str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index e3b880c92..ded7c14c2 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1017,7 +1017,6 @@ namespace pdr {
         TRACE("pdr_verbose", tout << "remove: " << n.level() << ": " << &n << " " << n.state() << "\n";);
         model_nodes& nodes = cache(n).find(n.state());
         nodes.erase(&n);
-        bool is_goal = n.is_goal();
         remove_goal(n);
         // TBD: siblings would also fail if n is not a goal.
         if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) {
diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h
index 4f8612d7f..8e5c09156 100644
--- a/src/muz/rel/karr_relation.h
+++ b/src/muz/rel/karr_relation.h
@@ -27,8 +27,8 @@ namespace datalog {
     class karr_relation;
 
     class karr_relation_plugin : public relation_plugin {
-        arith_util a;
         hilbert_basis m_hb;
+        arith_util a;
 
         class join_fn;
         class project_fn;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index f27043e8d..e34803b8a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -722,8 +722,6 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) {
 expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
     enode_pair_dependency* deps = 0;
     expr_dep ed;
-    expr* r = 0;
-
     if (m_rep.find_cache(e, ed)) {
         eqs = m_dm.mk_join(eqs, ed.second);
         return expr_ref(ed.first, m);
@@ -819,7 +817,8 @@ void theory_seq::deque_axiom(expr* n) {
         add_length_concat_axiom(n);
     }
     else if (m_util.str.is_string(n)) {
-        add_length_string_axiom(n);
+        add_elim_string_axiom(n);
+        // add_length_string_axiom(n);
     }
 }
 
@@ -956,6 +955,18 @@ void theory_seq::add_length_empty_axiom(expr* n) {
     add_axiom(mk_eq(len, zero, false));
 }
 
+void theory_seq::add_elim_string_axiom(expr* n) {
+    zstring s;
+    VERIFY(m_util.str.is_string(n, s));
+    SASSERT(s.length() > 0);
+    expr_ref result = m_util.str.mk_unit(m_util.str.mk_char(s, 0));
+    for (unsigned i = 1; i < s.length(); ++i) {
+        result = m_util.str.mk_concat(result, m_util.str.mk_unit(m_util.str.mk_unit_char(s, i)));
+    }
+    add_axiom(mk_eq(n, result, false));
+    m_rep.update(n, result, 0);
+}
+
 void theory_seq::add_length_string_axiom(expr* n) {
     if (!m_has_length) return;
     zstring s;
@@ -1038,7 +1049,6 @@ void theory_seq::add_extract_axiom(expr* e) {
     expr_ref zero(m_autil.mk_int(0), m);
     
     literal i_ge_0  = mk_literal(m_autil.mk_ge(i, zero));
-    literal i_le_l  = mk_literal(m_autil.mk_le(mk_sub(i, l), zero));
     literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
     literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero));
     literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index c25d2d7ff..b2b45e77e 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -63,7 +63,7 @@ namespace smt {
             void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
         public:
             solution_map(ast_manager& m, enode_pair_dependency_manager& dm): 
-                m(m), m_cache(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
+                m(m),  m_dm(dm), m_cache(m), m_lhs(m), m_rhs(m) {}
             bool empty() const { return m_map.empty(); }
             void  update(expr* e, expr* r, enode_pair_dependency* d);
             void  add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); }
@@ -206,6 +206,7 @@ namespace smt {
         void add_length_empty_axiom(expr* n);
         void add_length_concat_axiom(expr* n);
         void add_length_string_axiom(expr* n);
+        void add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
         literal mk_literal(expr* n);
         void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);