diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 33c1448e7..37197e730 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -935,7 +935,6 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
-        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         family_id fid = mk_c(c)->get_fpa_fid();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
@@ -1037,7 +1036,6 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();
-        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
         family_id fid = mk_c(c)->get_fpa_fid();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         SASSERT(plugin != 0);
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index f312da051..231326107 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -127,13 +127,13 @@ public class Solver extends Z3Object
      * using the Boolean constants in ps.
      *
      * Remarks: 
-     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * This API is an alternative to {@link check} with assumptions for
      * extracting unsat cores.
      * Both APIs can be used in the same solver. The unsat core will contain a
      * combination
-     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * of the Boolean variables provided using {@link assertAndTrack}
      * and the Boolean literals
-     * provided using <see cref="Check"/> with assumptions.
+     * provided using {@link check} with assumptions.
      **/
     public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
     {
@@ -152,13 +152,13 @@ public class Solver extends Z3Object
      * using the Boolean constant p.
      * 
      * Remarks: 
-     * This API is an alternative to <see cref="Check"/> with assumptions for
+     * This API is an alternative to {@link check} with assumptions for
      * extracting unsat cores.
      * Both APIs can be used in the same solver. The unsat core will contain a
      * combination
-     * of the Boolean variables provided using <see cref="AssertAndTrack"/>
+     * of the Boolean variables provided using {@link assertAndTrack}
      * and the Boolean literals
-     * provided using <see cref="Check"/> with assumptions.
+     * provided using {@link check} with assumptions.
      */ 
     public void assertAndTrack(BoolExpr constraint, BoolExpr p)
     {
@@ -294,7 +294,7 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Create a clone of the current solver with respect to <c>ctx</c>.
+     * Create a clone of the current solver with respect to{@code ctx}.
      */
     public Solver translate(Context ctx) 
     {
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 0dba6039c..861fb997d 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -634,9 +634,6 @@ struct app_flags {
     unsigned     m_ground:1;   // application does not have free variables or nested quantifiers.
     unsigned     m_has_quantifiers:1; // application has nested quantifiers.
     unsigned     m_has_labels:1; // application has nested labels.
-    static app_flags mk_const_flags();
-    static app_flags mk_default_app_flags();
-    static app_flags mk_default_quantifier_flags();
 };
 
 class app : public expr {
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 05edb35c8..3215840bc 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -140,8 +140,8 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
         return zstring(*this);
     }
     bool found = false;
-    for (unsigned i = 0; i <= length() - src.length(); ++i) {
-        bool eq = !found;
+    for (unsigned i = 0; i < length(); ++i) {
+        bool eq = !found && i + src.length() <= length();
         for (unsigned j = 0; eq && j < src.length(); ++j) {
             eq = m_buffer[i+j] == src[j];
         }
@@ -154,9 +154,6 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
             result.m_buffer.push_back(m_buffer[i]);
         }
     }
-    for (unsigned i = length() - src.length() + 1; i < length(); ++i) {
-        result.m_buffer.push_back(m_buffer[i]);
-    }
     return result;
 }
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 16f883548..23e1f746d 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -26,17 +26,17 @@ namespace smt {
 
     class fpa2bv_conversion_trail_elem : public trail<theory_fpa> {
         ast_manager & m;
-        obj_map<expr, expr*> & m_conversions;
-        expr * m_e;
+        obj_map<expr, expr*> & m_map;
+        expr_ref key;
     public:
-        fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & c, expr * e) :
-            m(m), m_conversions(c), m_e(e) { m.inc_ref(e); }
-        virtual ~fpa2bv_conversion_trail_elem() {}
+        fpa2bv_conversion_trail_elem(ast_manager & m, obj_map<expr, expr*> & map, expr * e) :
+            m(m), m_map(map), key(e, m) { }
+        virtual ~fpa2bv_conversion_trail_elem() { }
         virtual void undo(theory_fpa & th) {
-            expr * v = m_conversions.find(m_e);
-            m_conversions.remove(m_e);
-            m.dec_ref(v);
-            m.dec_ref(m_e);
+            expr * val = m_map.find(key);
+            m_map.remove(key);
+            m.dec_ref(val);
+            key = 0;
         }
     };
 
@@ -153,6 +153,8 @@ namespace smt {
 
     theory_fpa::~theory_fpa()
     {
+        m_trail_stack.reset();
+
         if (m_is_initialized) {
             ast_manager & m = get_manager();
             dec_ref_map_values(m, m_conversions);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index df96f9c20..e11ca806a 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -266,6 +266,16 @@ bool theory_seq::branch_variable() {
     context& ctx = get_context();
     unsigned sz = m_eqs.size();
     int start = ctx.get_random_value();
+
+    for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[(i + start) % m_eqs.size()];
+        if (reduce_length_eq(e.ls(), e.rs(), e.dep())) {
+            TRACE("seq", tout << "length\n";);
+            return true;
+        }
+    }
+
+
     unsigned s = 0;
     for (unsigned i = 0; i < sz; ++i) {
         unsigned k = (i + start) % sz;
@@ -488,6 +498,7 @@ bool theory_seq::check_length_coherence(expr* e) {
 }
 
 bool theory_seq::check_length_coherence() {
+
     obj_hashtable<expr>::iterator it = m_length.begin(), end = m_length.end();
     for (; it != end; ++it) {
         expr* e = *it;
@@ -822,24 +833,9 @@ 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, literal_vector& lits) {
 
-    rational val1, val2;
-    if (has_length(l) && has_length(r) && 
-        get_length(l, val1) && get_length(r, val2) && val1 == val2) {
-        context& ctx = get_context();
-        expr_ref len1(m_util.str.mk_length(l), m);
-        expr_ref len2(m_util.str.mk_length(r), m);
-        literal lit = mk_eq(len1, len2, false);
-        if (ctx.get_assignment(lit) == l_true) {
-            lits.push_back(lit);
-            return true;
-        }
-        else {
-            TRACE("seq", tout << "Assignment: " << len1 << " = " << len2 << " " << ctx.get_assignment(lit) << "\n";);
-            return false;
-        }
-    }
     expr_ref len1(m), len2(m);
     lits.reset();
     if (get_length(l, len1, lits) &&
@@ -962,10 +958,6 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
         TRACE("seq", tout << "unit\n";);
         return true;
     }
-    if (!ctx.inconsistent() && reduce_length_eq(ls, rs, deps)) {
-        TRACE("seq", tout << "length\n";);
-        return true;
-    }
     if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) {
         TRACE("seq", tout << "binary\n";);
         return true;
@@ -1027,6 +1019,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con
         lhs.append(ls.size()-1, ls.c_ptr() + 1);
         rhs.append(rs.size()-1, rs.c_ptr() + 1);
         SASSERT(!lhs.empty() || !rhs.empty());
+        deps = mk_join(deps, lits);
         m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
         TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
         propagate_eq(deps, lits, l, r, true);
@@ -1039,14 +1032,91 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con
         lhs.append(ls.size()-1, ls.c_ptr());
         rhs.append(rs.size()-1, rs.c_ptr());
         SASSERT(!lhs.empty() || !rhs.empty());
+        deps = mk_join(deps, lits);
         m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
         TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";);
         propagate_eq(deps, lits, l, r, true);
         return true;
     }
 
+    rational len1, len2, len;
+    if (ls.size() > 1 && get_length(ls[0], len1) && get_length(rs[0], len2) && len1 >= len2) {
+        unsigned j = 1; 
+        for (; j < rs.size() && len1 > len2 && get_length(rs[j], len); ++j) { 
+            len2 += len; 
+        }
+        if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(1, j, true, ls, rs, deps)) {
+            return true;
+        }
+    }
+    if (rs.size() > 1 && get_length(rs[0], len1) && get_length(ls[0], len2) && len1 > len2) {
+        unsigned j = 1; 
+        for (; j < ls.size() && len1 > len2 && get_length(ls[j], len); ++j) { 
+            len2 += len; 
+        }
+        if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(j, 1, true, ls, rs, deps)) {
+            return true;
+        }
+    }
+    if (ls.size() > 1 && get_length(ls.back(), len1) && get_length(rs.back(), len2) && len1 >= len2) {
+        unsigned j = rs.size()-1; 
+        for (; j > 0 && len1 > len2 && get_length(rs[j-1], len); --j) { 
+            len2 += len; 
+        }
+        if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(ls.size()-1, rs.size()-j, false, ls, rs, deps)) {
+            return true;
+        }
+    }
+    if (rs.size() > 1 && get_length(rs.back(), len1) && get_length(ls.back(), len2) && len1 > len2) {
+        unsigned j = ls.size()-1; 
+        for (; j > 0 && len1 > len2 && get_length(ls[j-1], len); --j) { 
+            len2 += len; 
+        }
+        if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(ls.size()-j, rs.size()-1, false, ls, rs, deps)) {
+            return true;
+        }
+    }
     return false;
- }
+}
+
+bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) {   
+    context& ctx = get_context();
+    expr* const* ls1 = ls.c_ptr();
+    expr* const* ls2 = ls.c_ptr()+i;
+    expr* const* rs1 = rs.c_ptr();
+    expr* const* rs2 = rs.c_ptr()+j;
+    unsigned l1 = i;
+    unsigned l2 = ls.size()-i;
+    unsigned r1 = j;
+    unsigned r2 = rs.size()-j;
+    if (!front) {
+        std::swap(ls1, ls2);
+        std::swap(rs1, rs2);
+        std::swap(l1, l2);
+        std::swap(r1, r2);        
+    }
+    SASSERT(0 < l1 && l1 < ls.size());
+    SASSERT(0 < r1 && r1 < rs.size());
+    expr_ref l(m_util.str.mk_concat(l1, ls1), m);
+    expr_ref r(m_util.str.mk_concat(r1, rs1), m);            
+    expr_ref lenl(m_util.str.mk_length(l), m);
+    expr_ref lenr(m_util.str.mk_length(r), m);
+    literal lit = mk_eq(lenl, lenr, false);
+    if (ctx.get_assignment(lit) == l_true) {
+        literal_vector lits;
+        expr_ref_vector lhs(m), rhs(m);
+        lhs.append(l2, ls2);
+        rhs.append(r2, rs2);
+        deps = mk_join(deps, lit);
+        m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps));
+        propagate_eq(deps, lits, l, r, true);
+        return true;
+    }
+    else {
+        //TRACE("seq", tout << "Assignment: " << lenl << " = " << lenr << " " << ctx.get_assignment(lit) << "\n";);
+        return false;
+    }
+}
 
 bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) {
     context& ctx = get_context();
@@ -1191,9 +1261,6 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
         len = m_autil.mk_int(1);
         return true;
     }
-    else {
-        TRACE("seq", tout << "unhandled: " << mk_pp(e, m) << "\n";);
-    }
     return false;    
 }
 
@@ -2314,7 +2381,10 @@ bool theory_seq::get_length(expr* e, rational& val) {
         else if (m_util.str.is_string(c, s)) {
             val += rational(s.length());
         }
-        else {
+        else if (!has_length(c)) {
+            return false;            
+        }
+        else {            
             len = m_util.str.mk_length(c);
             if (ctx.e_internalized(len) &&
                 tha->get_value(ctx.get_enode(len), len_val) &&
@@ -2322,7 +2392,6 @@ bool theory_seq::get_length(expr* e, rational& val) {
                 val += val1;
             }
             else {
-                TRACE("seq", tout << "No length provided for " << len << "\n";);
                 return false;
             }
         }
@@ -2595,8 +2664,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
 }
 
 
-expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1,
-                               expr* e2, expr* e3, sort* range) {
+expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, sort* range) {
     expr* es[3] = { e1, e2, e3 };
     unsigned len = e3?3:(e2?2:1);
     if (!range) {
@@ -2609,6 +2677,17 @@ 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;
 }
 
+theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal lit) {
+    return m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
+}
+
+theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal_vector const& lits) {
+    for (unsigned i = 0; i < lits.size(); ++i) {
+        deps = mk_join(deps, lits[i]);
+    } 
+    return deps;
+}
+
 void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) {
     literal_vector lits;
     lits.push_back(lit);
@@ -2631,11 +2710,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
     linearize(deps, eqs, lits);
 
     if (add_to_eqs) {
-        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)));
-        }
+        deps = mk_join(deps, _lits);
         new_eq_eh(deps, n1, n2);
     }
     TRACE("seq",
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index f0445aada..a28458e02 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -337,6 +337,7 @@ namespace smt {
         bool get_length(expr* s, expr_ref& len, literal_vector& lits);
         bool reduce_length(expr* l, expr* r, literal_vector& lits);
         bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
+        bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
 
         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); }
@@ -429,6 +430,10 @@ namespace smt {
         void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
         expr_ref mk_sub(expr* a, expr* b);
         enode* ensure_enode(expr* a);
+        
+        dependency* mk_join(dependency* deps, literal lit);
+        dependency* mk_join(dependency* deps, literal_vector const& lits);
+
 
         // arithmetic integration
         bool lower_bound(expr* s, rational& lo);