diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index fd79aa46e..1494b3afd 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -28,12 +28,13 @@ using namespace smt;
 theory_seq::theory_seq(ast_manager& m):
     theory(m.mk_family_id("seq")), 
     m(m),
+    m_dam(m_dep_array_value_manager, m_alloc),
     m_rep(m),    
     m_eqs_head(0),
     m_ineqs(m),
     m_axioms(m),
     m_axioms_head(0),
-    m_used(false), 
+    m_incomplete(false), 
     m_rewrite(m), 
     m_util(m),
     m_autil(m),
@@ -41,59 +42,48 @@ theory_seq::theory_seq(ast_manager& m):
     m_find(*this) {
     m_lhs.push_back(expr_array());
     m_rhs.push_back(expr_array());
+    m_deps.push_back(enode_pair_dependency_array());
 }
 
 final_check_status theory_seq::final_check_eh() { 
     context & ctx   = get_context();
-    final_check_status st = check_ineqs();
-    if (st == FC_CONTINUE) {
+    if (!check_ineqs()) {
         return FC_CONTINUE;
     }
-    return m_used?FC_GIVEUP:FC_DONE; 
+    if (simplify_and_solve_eqs()) {
+        return FC_CONTINUE;
+    }
+    if (m.size(m_lhs.back()) > 0) {
+        return FC_GIVEUP;        
+    }
+    return m_incomplete?FC_GIVEUP:FC_DONE; 
 }
 
-final_check_status theory_seq::check_ineqs() {
+bool theory_seq::check_ineqs() {
     context & ctx   = get_context();
-    enode_pair_vector eqs;
     for (unsigned i = 0; i < m_ineqs.size(); ++i) {
         expr_ref a(m_ineqs[i].get(), m);
+        enode_pair_dependency* eqs = 0;
         expr_ref b = canonize(a, eqs);
         if (m.is_true(b)) {
             ctx.internalize(a, false);
             literal lit(ctx.get_literal(a));
             ctx.mark_as_relevant(lit);
+            vector<enode_pair, false> _eqs;
+            m_dm.linearize(eqs, _eqs);
             ctx.assign(
                 lit, 
                 ctx.mk_justification(
                     ext_theory_propagation_justification(
-                        get_id(), ctx.get_region(), 0, 0, eqs.size(), eqs.c_ptr(), lit)));
-            return FC_CONTINUE;
+                        get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit)));
+            return false;
         }
     }
-    return FC_DONE;
+    return true;
 }
 
-bool theory_seq::simplify_eqs() {
-    context & ctx   = get_context();
-    bool simplified = false;
-    expr_array& lhs = m_lhs.back();
-    expr_array& rhs = m_rhs.back();
-    for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) {
-        if (simplify_eq(m.get(lhs, i), m.get(rhs, i), m_deps)) {
-            if (i + 1 != m.size(lhs)) {
-                m.set(lhs, i, m.get(lhs, m.size(lhs)-1));
-                m.set(rhs, i, m.get(rhs, m.size(rhs)-1));
-                --i;
-                simplified = true;
-            }
-            m.pop_back(lhs);
-            m.pop_back(rhs);
-        }
-    }
-    return simplified;
-}
 
-bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) {
+bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) {
     context& ctx = get_context();
     seq_rewriter rw(m);
     expr_ref_vector lhs(m), rhs(m);
@@ -107,11 +97,13 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) {
         expr_ref a(m);
         a = m.mk_eq(l, r);
         literal lit(ctx.get_literal(a));
+        vector<enode_pair, false> _eqs;
+        m_dm.linearize(deps, _eqs);
         ctx.assign(
             ~lit,
             ctx.mk_justification(
                 ext_theory_propagation_justification(
-                    get_id(), ctx.get_region(), 0, 0, deps.size(), deps.c_ptr(), ~lit)));
+                    get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), ~lit)));
         return true;
     }
     if (lhs.size() == 1 && l == lhs[0].get() &&
@@ -122,11 +114,96 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) {
     for (unsigned i = 0; i < lhs.size(); ++i) {
         m.push_back(m_lhs.back(), lhs[i].get());
         m.push_back(m_rhs.back(), rhs[i].get());
-        // TBD m_deps.push_back(deps);
+        m_dam.push_back(m_deps.back(), deps);
     }    
     return true;
 }
 
+bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) {
+    expr_ref lh = canonize(l, deps);
+    expr_ref rh = canonize(r, deps);
+    if (is_var(lh) && !occurs(lh, rh)) {
+        add_solution(lh, rh, deps);
+        return true;
+    }
+    if (is_var(rh) && !occurs(rh, lh)) {
+        add_solution(rh, lh, deps);
+        return true;
+    }
+    // Use instead reference counts for dependencies to GC?
+
+    return false;
+}
+
+bool theory_seq::occurs(expr* a, expr* b) {
+    // TBD
+    return true;
+}
+
+bool theory_seq::is_var(expr* a) {
+    // TBD
+    return false;
+}
+
+void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
+    context& ctx = get_context();
+    // TBD: internalize lh, rh;
+    // 
+    enode* n1 = ctx.get_enode(l);
+    enode* n2 = ctx.get_enode(r);
+    // TBD: add substitution l -> r
+    vector<enode_pair, false> _eqs;
+    m_dm.linearize(deps, _eqs);
+    // alloc?
+    ctx.assign_eq(n1, n2, eq_justification(
+                      alloc(ext_theory_eq_propagation_justification,
+                            get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)));
+}
+
+bool theory_seq::simplify_eqs() {
+    return pre_process_eqs(true);
+}
+
+bool theory_seq::solve_basic_eqs() {
+    return pre_process_eqs(false);
+}
+
+bool theory_seq::pre_process_eqs(bool simplify_or_solve) {
+    context& ctx = get_context();
+    bool change = false;
+    expr_array& lhs = m_lhs.back();
+    expr_array& rhs = m_rhs.back();
+    enode_pair_dependency_array& deps = m_deps.back();
+    for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) {
+        if (simplify_or_solve?
+            simplify_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i)):
+            solve_unit_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i))) {  
+            if (i + 1 != m.size(lhs)) {
+                m.set(lhs, i, m.get(lhs, m.size(lhs)-1));
+                m.set(rhs, i, m.get(rhs, m.size(rhs)-1));
+                m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1));
+                --i;
+                change = true;
+            }
+            m.pop_back(lhs);
+            m.pop_back(rhs);
+            m_dam.pop_back(deps);
+        }
+    }    
+    return change;
+}
+
+bool theory_seq::simplify_and_solve_eqs() {
+    context & ctx   = get_context();
+    bool change = simplify_eqs();
+    while (!ctx.inconsistent() && solve_basic_eqs()) {
+        simplify_eqs();
+        change = true;
+    }
+    return change;
+}
+
+
 final_check_status theory_seq::add_axioms() {
     for (unsigned i = 0; i < get_num_vars(); ++i) {
 
@@ -140,7 +217,6 @@ bool theory_seq::internalize_atom(app* a, bool) {
 }
 
 bool theory_seq::internalize_term(app* term) { 
-    m_used = true;
     context & ctx   = get_context();
     unsigned num_args = term->get_num_args();
     for (unsigned i = 0; i < num_args; i++) {
@@ -159,11 +235,26 @@ bool theory_seq::internalize_term(app* term) {
         theory_var v = mk_var(e);
         ctx.attach_th_var(e, this, v);
     }
+    if (!m_util.str.is_concat(term) &&
+        !m_util.str.is_string(term) &&
+        !m_util.str.is_suffix(term) &&
+        !m_util.str.is_prefix(term) &&
+        !m_util.str.is_contains(term)) {
+        set_incomplete(term);
+    }
+        
     // assert basic axioms    
-    if (!m_used) { m_trail_stack.push(value_trail<theory_seq,bool>(m_used)); m_used = true; } 
     return true;
 }
 
+void theory_seq::set_incomplete(app* term) {
+    TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";);
+    if (!m_incomplete) { 
+        m_trail_stack.push(value_trail<theory_seq,bool>(m_incomplete)); 
+        m_incomplete = true; 
+    } 
+}
+
 theory_var theory_seq::mk_var(enode* n) {
     theory_var r = theory::mk_var(n);
     VERIFY(r == m_find.mk_var());
@@ -175,14 +266,13 @@ bool theory_seq::can_propagate() {
     return m_axioms_head < m_axioms.size();
 }
 
-expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) {
-    eqs.reset();
+expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) {
     expr_ref result = expand(e, eqs);
     m_rewrite(result);
     return result;
 }
 
-expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
+expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
     context& ctx = get_context();
     expr* e1, *e2;
     SASSERT(ctx.e_internalized(e));
@@ -191,27 +281,27 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
     do {
         e = n->get_owner();
         if (m_util.str.is_concat(e, e1, e2)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m);
         }        
         if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(e, m);
         }
         if (m.is_eq(e, e1, e2)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m);
         }
         if (m_util.str.is_prefix(e, e1, e2)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m);
         }
         if (m_util.str.is_suffix(e, e1, e2)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m);
         }
         if (m_util.str.is_contains(e, e1, e2)) {
-            if (start != n) eqs.push_back(enode_pair(start, n));
+            add_dependency(eqs, start, n);
             return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m);
         }
 #if 0
@@ -227,6 +317,20 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) {
     return expr_ref(n->get_root()->get_owner(), m);
 }
 
+void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) {
+    dep = join(dep, leaf(a, b));
+}
+
+theory_seq::enode_pair_dependency* theory_seq::join(enode_pair_dependency* a, enode_pair_dependency* b) {
+    if (!a) return b;
+    if (!b) return a;
+    return m_dm.mk_join(a, b);
+}
+
+theory_seq::enode_pair_dependency* theory_seq::leaf(enode* a, enode* b) {
+    return (a == b)?0:m_dm.mk_leaf(std::make_pair(a, b));
+}
+
 void theory_seq::propagate() {
     context & ctx = get_context();
     while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
@@ -328,26 +432,33 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
 
 void theory_seq::push_scope_eh() {
     theory::push_scope_eh();
+    m_dm.push_scope();
     m_trail_stack.push_scope();
     m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
     m_trail_stack.push(value_trail<theory_seq, unsigned>(m_eqs_head));
     expr_array lhs, rhs;
+    enode_pair_dependency_array deps;
     m.copy(m_lhs.back(), lhs);
     m.copy(m_rhs.back(), rhs);
+    m_dam.copy(m_deps.back(), deps);
     m_lhs.push_back(lhs);
     m_rhs.push_back(rhs);
+    m_deps.push_back(deps);
 }
 
 void theory_seq::pop_scope_eh(unsigned num_scopes) {
     m_trail_stack.pop_scope(num_scopes);
-    theory::pop_scope_eh(num_scopes);    
+    theory::pop_scope_eh(num_scopes);   
+    m_dm.pop_scope(num_scopes); 
     m_rep.resize(get_num_vars());
     while (num_scopes > 0) {
         --num_scopes;
         m.del(m_lhs.back());
         m.del(m_rhs.back());
+        m_dam.del(m_deps.back());
         m_lhs.pop_back();
         m_rhs.pop_back();
+        m_deps.pop_back();
     }
 }
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 3a7b978e9..236a34a04 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -28,6 +28,22 @@ Revision History:
 namespace smt {
 
     class theory_seq : public theory {
+        struct config {
+            static const bool preserve_roots   = true;
+            static const unsigned max_trail_sz = 16;
+            static const unsigned factor       = 2;
+            typedef small_object_allocator   allocator;
+        };
+        typedef scoped_dependency_manager<enode_pair> enode_pair_dependency_manager;
+        typedef enode_pair_dependency_manager::dependency enode_pair_dependency;
+        struct enode_pair_dependency_array_config : public config {
+            typedef enode_pair_dependency*      value;
+            typedef dummy_value_manager<value>  value_manager;
+            static const bool ref_count = false;
+        };
+        typedef parray_manager<enode_pair_dependency_array_config> enode_pair_dependency_array_manager;
+        typedef enode_pair_dependency_array_manager::ref enode_pair_dependency_array;
+        
         typedef union_find<theory_seq> th_union_find;
         typedef trail_stack<theory_seq> th_trail_stack;
         struct stats {
@@ -35,17 +51,23 @@ namespace smt {
             void reset() { memset(this, 0, sizeof(stats)); }
             unsigned m_num_splits;
         };
-        ast_manager&    m;
-        expr_ref_vector m_rep;        // unification representative.
-        vector<expr_array> m_lhs, m_rhs; // persistent sets of equalities.
-        unsigned        m_eqs_head;      // index of unprocessed equation.
-        enode_pair_vector m_deps;    // TBD - convert to dependency structure.
+        ast_manager&                        m;
+        small_object_allocator              m_alloc;
+        enode_pair_dependency_array_config::value_manager m_dep_array_value_manager;
+        enode_pair_dependency_manager       m_dm;
+        enode_pair_dependency_array_manager m_dam;
+        expr_ref_vector                     m_rep;        // unification representative.
+        vector<expr_array>                  m_lhs, m_rhs; // persistent sets of equalities.
+        vector<enode_pair_dependency_array> m_deps;
+
+        unsigned                            m_eqs_head;   // index of unprocessed equation. deprecate
+        
 
 
         expr_ref_vector m_ineqs;      // inequalities to check
         expr_ref_vector m_axioms;     
         unsigned        m_axioms_head;        
-        bool            m_used;       // deprecate
+        bool            m_incomplete; 
         th_rewriter     m_rewrite;
         seq_util        m_util;
         arith_util      m_autil;
@@ -69,18 +91,31 @@ namespace smt {
         virtual char const * get_name() const { return "seq"; }
         virtual theory_var mk_var(enode* n);
 
-        final_check_status check_ineqs();
+        bool check_ineqs();
+        bool pre_process_eqs(bool simplify_or_solve);
         bool simplify_eqs();
-        bool simplify_eq(expr* l, expr* r, enode_pair_vector& deps);
+        bool simplify_eq(expr* l, expr* r, enode_pair_dependency* deps);
+        bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps);
+        bool solve_basic_eqs();
+        bool simplify_and_solve_eqs();
+        bool occurs(expr* a, expr* b);
+        bool is_var(expr* b);
+        void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
+
         final_check_status add_axioms();
 
         void assert_axiom(expr_ref& e);
         void create_axiom(expr_ref& e);
-        expr_ref canonize(expr* e, enode_pair_vector& eqs);
-        expr_ref expand(expr* e, enode_pair_vector& eqs);
+        expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
+        expr_ref expand(expr* e, enode_pair_dependency*& eqs);
+        void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
+        enode_pair_dependency* leaf(enode* a, enode* b);
+        enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b);
 
         void propagate_eq(bool_var v, expr* e1, expr* e2);
         expr_ref mk_skolem(char const* name, expr* e1, expr* e2);
+
+        void set_incomplete(app* term);
     public:
         theory_seq(ast_manager& m);
         virtual void init_model(model_generator & mg) {