diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 3ead59833..8f7b56381 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1206,8 +1206,7 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
         e = todo.back();
         todo.pop_back();
         if (m_util.str.is_string(e, s)) {
-            for (unsigned i = s.length(); i > 0; ) {
-                --i;
+            for (unsigned i = 0; i < s.length(); ++i) {
                 seq.push_back(m_util.str.mk_char(s, i));
             }
         }
@@ -1218,14 +1217,13 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
             seq.push_back(e1);
         }
         else if (m_util.str.is_concat(e, e1, e2)) {
-            todo.push_back(e1);
             todo.push_back(e2);
+            todo.push_back(e1);
         }
         else {
             return false;
         }
     }
-    seq.reverse();
     return true;
 }
 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index b704795b2..2b2c35466 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2251,7 +2251,9 @@ bool theory_seq::internalize_term(app* term) {
         e = ctx.mk_enode(term, false, m.is_bool(term), true);
     }
     mk_var(e);
-
+    if (m_util.str.is_string(term)) {
+        add_elim_string_axiom(term);
+    }
     return true;
 }
 
@@ -3086,6 +3088,7 @@ void theory_seq::propagate() {
 
 void theory_seq::enque_axiom(expr* e) {
     if (!m_axiom_set.contains(e)) {
+        TRACE("seq", tout << "add axiom " << mk_pp(e, m) << "\n";);
         m_axioms.push_back(e);
         m_axiom_set.insert(e);
         m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
@@ -3285,13 +3288,13 @@ void theory_seq::add_replace_axiom(expr* r) {
 
 void theory_seq::add_elim_string_axiom(expr* n) {
     zstring s;
+    TRACE("seq", tout << mk_pp(n, m) << "\n";);
     VERIFY(m_util.str.is_string(n, s));
     if (s.length() == 0) {
         return;
     }
     expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m);
-    for (unsigned i = s.length()-1; i > 0; ) {
-        --i;
+    for (unsigned i = s.length()-1; i-- > 0; ) {
         result = mk_concat(m_util.str.mk_unit(m_util.str.mk_char(s, i)), result);
     }
     add_axiom(mk_eq(n, result, false));
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0ef008927..f2432b4fb 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8388,13 +8388,12 @@ namespace smt {
     lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) {
         app * target_term = to_app(get_manager().mk_not(m_theoryStrOverlapAssumption_term));
         get_context().internalize(target_term, false);
+		enode* e1 = get_context().get_enode(target_term);
         for (unsigned i = 0; i < unsat_core.size(); ++i) {
             app * core_term = to_app(unsat_core.get(i));
             // not sure if this is the correct way to compare terms in this context
-            enode * e1;
-            enode * e2;
-            e1 = get_context().get_enode(target_term);
-            e2 = get_context().get_enode(core_term);
+			if (!get_context().e_internalized(core_term)) continue;
+            enode *e2 = get_context().get_enode(core_term);
             if (e1 == e2) {
                 TRACE("str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;);
                 return l_undef;