diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 50fca7c1e..8c7d24461 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -211,9 +211,9 @@ theory_seq::theory_seq(ast_manager& m):
     m_indexof_left   = "seq.indexof.left";
     m_indexof_right  = "seq.indexof.right";
     m_aut_step       = "aut.step";
-    m_extract_prefix = "seq.extract.prefix";
-    m_at_left        = "seq.at.left";
-    m_at_right       = "seq.at.right";
+    m_pre            = "seq.pre";  // (seq.pre s l):  prefix of string s of length l
+    m_post           = "seq.post"; // (seq.post s l): suffix of string s of length l
+    m_eq             = "seq.eq";
 }
 
 theory_seq::~theory_seq() {
@@ -257,6 +257,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>is_solved\n";);
         return FC_DONE;
     }
+    TRACE("seq", tout << ">>give_up\n";);
     return FC_GIVEUP;
 }
 
@@ -528,11 +529,17 @@ bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
 }
 
 bool theory_seq::is_eq(expr* e, expr*& a, expr*& b) const {
-    return is_skolem(symbol("seq.eq"), e) &&
+    return is_skolem(m_eq, e) &&
         (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
 }
 
 
+bool theory_seq::is_pre(expr* e, expr*& s, expr*& i) {
+    return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
+}
+
+
+
 expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     sort* char_sort = 0;
     VERIFY(m_util.is_seq(m.get_sort(s), char_sort));
@@ -779,8 +786,10 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
         expr_ref li(lhs[i].get(), m);
         expr_ref ri(rhs[i].get(), m);
         if (solve_unit_eq(li, ri, deps)) {
+            // no-op
         }
         else if (m_util.is_seq(li) || m_util.is_re(li)) {
+            reduce_length(li, ri);
             m_eqs.push_back(mk_eqdep(li, ri, deps));
         }
         else {
@@ -808,6 +817,23 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const&
     return false;
 }
 
+bool theory_seq::reduce_length(expr* l, expr* r) {
+    expr* l2, *r2;
+    expr_ref len1(m), len2(m);
+    literal_vector lits;
+    m_util.str.is_concat(l, l, l2);
+    m_util.str.is_concat(r, r, r2);
+    if (get_length(l, len1, lits) &&
+        get_length(r, len2, lits) && len1 == len2) {
+        TRACE("seq", tout << "Propagate equal lengths\n";);
+        //propagate_eq(lits, l, r, true);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
 bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
     if (l == r) {
         return true;
@@ -1035,6 +1061,58 @@ bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector cons
     return false;
 }
 
+bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
+    context& ctx = get_context();
+    expr* s, *i, *l;
+    if (m_util.str.is_extract(e, s, i, l)) {
+        // 0 <= i <= len(s), 0 <= l, i + l <= len(s)
+        expr_ref zero(m_autil.mk_int(0), m);        
+        expr_ref ls(m_util.str.mk_length(s), m);
+        expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
+        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
+        literal li_ge_ls  = mk_literal(m_autil.mk_ge(ls_minus_i_l, zero));
+        literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
+        if (ctx.get_assignment(i_ge_0) == l_true &&
+            ctx.get_assignment(i_lt_len_s) == l_true && 
+            ctx.get_assignment(li_ge_ls) == l_true &&
+            ctx.get_assignment(l_ge_zero) == l_true) {
+            len = l;
+            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s); lits.push_back(li_ge_ls); lits.push_back(l_ge_zero);
+            return true;
+        }
+    }
+    else if (m_util.str.is_at(e, s, i)) {
+        // has length 1 if 0 <= i < len(s)
+        expr_ref zero(m_autil.mk_int(0), m);
+        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
+        if (ctx.get_assignment(i_ge_0) == l_true &&
+            ctx.get_assignment(i_lt_len_s) == l_true) {
+            len = m_autil.mk_int(1);
+            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
+            return true;
+        }
+    }
+    else if (is_pre(e, s, i)) {
+        expr_ref zero(m_autil.mk_int(0), m);
+        literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+        literal i_lt_len_s = ~mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
+        if (ctx.get_assignment(i_ge_0) == l_true &&
+            ctx.get_assignment(i_lt_len_s) == l_true) {
+            len = i;
+            lits.push_back(i_ge_0); lits.push_back(i_lt_len_s);
+            return true;
+        }
+    }
+    else if (m_util.str.is_unit(e)) {
+        len = m_autil.mk_int(1);
+        return true;
+    }
+    return false;    
+}
+
+
 bool theory_seq::solve_nqs(unsigned i) {
     context & ctx = get_context();
     for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
@@ -1499,12 +1577,34 @@ void theory_seq::display_disequation(std::ostream& out, ne const& e) const {
 }
 
 void theory_seq::display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const {
+    context& ctx = get_context();
+    smt2_pp_environment_dbg env(m);
+    params_ref p;
     for (unsigned i = 0; i < eqs.size(); ++i) {
-        out << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
+        out << "  (= ";
+        ast_smt2_pp(out, eqs[i].first->get_owner(), env, p, 5);
+        out << "\n     ";
+        ast_smt2_pp(out, eqs[i].second->get_owner(), env, p, 5);
+        out << ")\n";
     }
     for (unsigned i = 0; i < lits.size(); ++i) {
-        literal lit = lits[i];
-        get_context().display_literals_verbose(out, 1, &lit);
+        literal l = lits[i];        
+        if (l == true_literal) {
+            out << "   true";
+        }
+        else if (l == false_literal) {
+            out << "   false";
+        }
+        else {
+            expr* e = ctx.bool_var2expr(l.var());
+            if (l.sign()) {
+                ast_smt2_pp(out << "  (not ", e, env, p, 7);
+                out << ")";
+            }
+            else {
+                ast_smt2_pp(out << "  ", e, env, p, 2);
+            }
+        }
         out << "\n";
     }
 }
@@ -1513,14 +1613,7 @@ void theory_seq::display_deps(std::ostream& out, dependency* dep) const {
     literal_vector lits;
     enode_pair_vector eqs;
     linearize(dep, eqs, lits);
-    for (unsigned i = 0; i < eqs.size(); ++i) {
-        out << "   " << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
-    }
-    for (unsigned i = 0; i < lits.size(); ++i) {
-        literal lit = lits[i];
-        get_context().display_literals_verbose(out << "  ", 1, &lit);
-        out << "\n";
-    }
+    display_deps(out, lits, eqs);
 }
 
 void theory_seq::collect_statistics(::statistics & st) const {
@@ -2176,12 +2269,24 @@ void theory_seq::add_extract_axiom(expr* e) {
         add_tail_axiom(e, s);
         return;
     }
-    expr_ref x(mk_skolem(m_extract_prefix, s, e), m);
-    expr_ref y(mk_skolem(symbol("seq.extract.suffix"), s, e), m);
+    if (is_drop_last(s, i, l)) {
+        add_drop_last_axiom(e, s);
+        return;
+    }
+    if (is_extract_prefix0(s, i, l)) {
+        add_extract_prefix_axiom(e, s, l);
+        return;
+    }
+    if (is_extract_suffix(s, i, l)) {
+        add_extract_suffix_axiom(e, s, i);
+        return;
+    }
+    expr_ref x(mk_skolem(m_pre, s, i), m);
     expr_ref ls(m_util.str.mk_length(s), m);
     expr_ref lx(m_util.str.mk_length(x), m);
     expr_ref le(m_util.str.mk_length(e), m);
-    expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i),l), m);
+    expr_ref ls_minus_i_l(mk_sub(mk_sub(ls, i), l), m);
+    expr_ref y(mk_skolem(m_post, s, ls_minus_i_l), m);
     expr_ref xe = mk_concat(x, e);
     expr_ref xey = mk_concat(x, e, y);
     expr_ref zero(m_autil.mk_int(0), m);
@@ -2202,8 +2307,23 @@ void theory_seq::add_extract_axiom(expr* e) {
 void theory_seq::add_tail_axiom(expr* e, expr* s) {
     expr_ref head(m), tail(m);
     mk_decompose(s, head, tail);
-    add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(head, tail)));
-    add_axiom(mk_eq_empty(s), mk_seq_eq(e, tail));
+    add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(head, e)));
+}
+
+void theory_seq::add_drop_last_axiom(expr* e, expr* s) {
+    add_axiom(mk_eq_empty(s), mk_seq_eq(s, mk_concat(e, m_util.str.mk_unit(mk_last(s)))));
+}
+
+bool theory_seq::is_drop_last(expr* s, expr* i, expr* l) {
+    rational i1;
+    if (!m_autil.is_numeral(i, i1) || !i1.is_zero()) {
+        return false;
+    }
+    expr_ref l2(m), l1(l, m);
+    l2 = m_autil.mk_sub(m_util.str.mk_length(s), m_autil.mk_int(1));
+    m_rewrite(l1);
+    m_rewrite(l2);
+    return l1 == l2;
 }
 
 bool theory_seq::is_tail(expr* s, expr* i, expr* l) {
@@ -2213,10 +2333,54 @@ bool theory_seq::is_tail(expr* s, expr* i, expr* l) {
     }
     expr_ref l2(m), l1(l, m);
     l2 = m_autil.mk_sub(m_util.str.mk_length(s), m_autil.mk_int(1));
-    m_rewrite(l2);
     m_rewrite(l1);
+    m_rewrite(l2);
     return l1 == l2;
 }
+
+bool theory_seq::is_extract_prefix0(expr* s, expr* i, expr* l) {
+    rational i1;
+    return m_autil.is_numeral(i, i1) && i1.is_zero();    
+}
+
+bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
+    expr_ref len(m_autil.mk_add(l, i), m);
+    m_rewrite(len);
+    return m_util.str.is_length(len, l) && l == s;
+}
+
+/*
+  0 <= l <= len(s) => s = ey & l = len(e)
+ */
+void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
+    expr_ref le(m_util.str.mk_length(e), m);
+    expr_ref ls(m_util.str.mk_length(s), m);
+    expr_ref ls_minus_l(mk_sub(ls, l), m);
+    expr_ref y(mk_skolem(m_post, s, ls_minus_l), m);
+    expr_ref zero(m_autil.mk_int(0), m);
+    expr_ref ey = mk_concat(e, y);
+    literal l_ge_0 = mk_literal(m_autil.mk_ge(l, zero));
+    literal l_le_s = mk_literal(m_autil.mk_le(mk_sub(l, ls), zero));
+    add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
+    add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
+}
+
+/*
+  0 <= i <= len(s) => s = xe & i = len(x)    
+ */
+void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
+    expr_ref x(mk_skolem(m_pre, s, i), m);
+    expr_ref lx(m_util.str.mk_length(x), m);
+    expr_ref ls(m_util.str.mk_length(s), m);
+    expr_ref zero(m_autil.mk_int(0), m);
+    expr_ref xe = mk_concat(x, e);
+    literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
+    literal i_le_s = mk_literal(m_autil.mk_le(mk_sub(i, ls), zero));
+    add_axiom(~i_ge_0, ~i_le_s, mk_seq_eq(s, xe));
+    add_axiom(~i_ge_0, ~i_le_s, mk_eq(i, lx, false));
+}
+
+
 /*
    let e = at(s, i)
 
@@ -2226,14 +2390,14 @@ bool theory_seq::is_tail(expr* s, expr* i, expr* l) {
 void theory_seq::add_at_axiom(expr* e) {
     expr* s, *i;
     VERIFY(m_util.str.is_at(e, s, i));
-    expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
-    x     = mk_skolem(m_at_left, s, i);
-    y     = mk_skolem(m_at_right, s, i);
-    xey   = mk_concat(x, e, y);
-    zero  = m_autil.mk_int(0);
-    one   = m_autil.mk_int(1);
-    len_e = m_util.str.mk_length(e);
-    len_x = m_util.str.mk_length(x);
+    expr_ref len_e(m_util.str.mk_length(e), m);
+    expr_ref len_s(m_util.str.mk_length(s), m);
+    expr_ref zero(m_autil.mk_int(0), m);
+    expr_ref one(m_autil.mk_int(1), m);
+    expr_ref x = mk_skolem(m_pre, s, i);
+    expr_ref y = mk_skolem(m_post, s, mk_sub(mk_sub(len_s, i), one));
+    expr_ref xey   = mk_concat(x, e, y);
+    expr_ref len_x(m_util.str.mk_length(x), m);
 
     literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
     literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
@@ -2300,7 +2464,7 @@ literal theory_seq::mk_literal(expr* _e) {
 
 literal theory_seq::mk_seq_eq(expr* a, expr* b) {
     SASSERT(m_util.is_seq(a));
-    return mk_literal(mk_skolem(symbol("seq.eq"), a, b, 0, m.mk_bool_sort()));
+    return mk_literal(mk_skolem(m_eq, a, b, 0, m.mk_bool_sort()));
 }
 
 literal theory_seq::mk_eq_empty(expr* _e) {
@@ -2359,8 +2523,13 @@ bool theory_seq::is_skolem(symbol const& s, expr* e) const {
     return m_util.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s;
 }
 
-
 void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) {
+    literal_vector lits;
+    lits.push_back(lit);
+    propagate_eq(lits, e1, e2, add_to_eqs);
+}
+
+void theory_seq::propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs) {
     context& ctx = get_context();
 
     enode* n1 = ensure_enode(e1);
@@ -2371,18 +2540,21 @@ void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs)
     ctx.mark_as_relevant(n1);
     ctx.mark_as_relevant(n2);
     if (add_to_eqs) {
-        SASSERT(l_true == ctx.get_assignment(lit));
-        dependency* deps = m_dm.mk_leaf(assumption(lit));
+        dependency* deps = 0;
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            literal lit = lits[i];
+            SASSERT(l_true == ctx.get_assignment(lit));
+            deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
+        }
         new_eq_eh(deps, n1, n2);
-
     }
     TRACE("seq",
-          ctx.display_literals_verbose(tout, 1, &lit);
+          ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
           tout << " => " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
     justification* js =
         ctx.mk_justification(
             ext_theory_eq_propagation_justification(
-                get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2));
+                get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, n1, n2));
 
     m_new_propagation = true;
     ctx.assign_eq(n1, n2, eq_justification(js));
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index a05d056ea..3f636347d 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -276,7 +276,7 @@ namespace smt {
         stats            m_stats;
         symbol           m_prefix, m_suffix, m_contains_left, m_contains_right, m_accept, m_reject;
         symbol           m_tail, m_nth, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
-        symbol           m_extract_prefix, m_at_left, m_at_right;
+        symbol           m_pre, m_post, m_eq;
         ptr_vector<expr> m_todo;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
@@ -334,6 +334,9 @@ namespace smt {
         bool solve_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
         bool propagate_max_length(expr* l, expr* r, dependency* dep);
 
+        bool get_length(expr* s, expr_ref& len, literal_vector& lits);
+        bool reduce_length(expr* l, expr* r);
+
         expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
         expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
         expr_ref mk_concat(expr_ref_vector const& es, sort* s) { if (es.empty()) return mk_empty(s); return mk_concat(es.size(), es.c_ptr()); }
@@ -362,6 +365,7 @@ namespace smt {
         void propagate_lit(dependency* dep, unsigned n, literal const* lits, literal lit);
         void propagate_eq(dependency* dep, enode* n1, enode* n2);
         void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs);
+        void propagate_eq(literal_vector const& lits, expr* e1, expr* e2, bool add_to_eqs);
         void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
         u_map<unsigned> m_branch_start;
@@ -379,6 +383,7 @@ namespace smt {
         bool is_nth(expr* a) const;
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
         bool is_eq(expr* e, expr*& a, expr*& b) const; 
+        bool is_pre(expr* e, expr*& s, expr*& i);
         expr_ref mk_nth(expr* s, expr* idx);
         expr_ref mk_last(expr* e);
         expr_ref mk_first(expr* e);
@@ -399,7 +404,14 @@ namespace smt {
         void add_extract_axiom(expr* e);
         void add_length_axiom(expr* n);
         void add_tail_axiom(expr* e, expr* s);
+        void add_drop_last_axiom(expr* e, expr* s);
+        void add_extract_prefix_axiom(expr* e, expr* s, expr* l);
+        void add_extract_suffix_axiom(expr* e, expr* s, expr* i);
         bool is_tail(expr* s, expr* i, expr* l);
+        bool is_drop_last(expr* s, expr* i, expr* l);
+        bool is_extract_prefix0(expr* s, expr* i, expr* l);
+        bool is_extract_suffix(expr* s, expr* i, expr* l);
+        
 
         bool has_length(expr *e) const { return m_length.contains(e); }
         void add_length(expr* e);