diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp
index ee391f14a..b39c8368a 100644
--- a/src/api/api_stats.cpp
+++ b/src/api/api_stats.cpp
@@ -130,4 +130,8 @@ extern "C" {
         Z3_CATCH_RETURN(0.0);
     }
 
+    __uint64 Z3_API Z3_get_estimated_alloc_size(void) {
+        return memory::get_allocation_size();
+    }
+
 };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 528399394..b37c963b4 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4419,6 +4419,9 @@ extern "C" {
         \brief Interface to simplifier.
 
         Provides an interface to the AST simplifier used by Z3.
+        It returns an AST object which is equal to the argument.
+        The returned AST is simplified using algebraic simplificaiton rules, 
+        such as constant propagation (propagating true/false over logical connectives).         
 
         def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))
     */
@@ -5964,6 +5967,13 @@ extern "C" {
     */
     double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx);
 
+    /**
+    \brief Return the estimated allocated memory in bytes.
+
+    def_API('Z3_get_estimated_alloc_size', UINT64, ())
+    */
+    __uint64 Z3_API Z3_get_estimated_alloc_size(void);
+
     /*@}*/
 
 #ifdef __cplusplus
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 16aef6a00..53f058fb4 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -743,7 +743,14 @@ void bit_blaster_tpl<Cfg>::mk_srem(unsigned sz, expr * const * a_bits, expr * co
         mk_abs(sz, a_bits, abs_a_bits);
         mk_abs(sz, b_bits, abs_b_bits);
         expr_ref_vector urem_bits(m());
-        mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
+        numeral n_b;
+        unsigned shift;
+        // a urem 2^n -> a & ((2^n)-1)
+        if (is_numeral(sz, abs_b_bits.c_ptr(), n_b) && n_b.is_power_of_two(shift)) {
+            mk_zero_extend(shift, abs_a_bits.c_ptr(), sz - shift, urem_bits);
+        } else {
+            mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
+        }
         expr_ref_vector neg_urem_bits(m());
         mk_neg(sz, urem_bits.c_ptr(), neg_urem_bits);
         mk_multiplexer(a_msb, sz, neg_urem_bits.c_ptr(), urem_bits.c_ptr(), out_bits);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 1b1d6c450..911914a4d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -36,6 +36,7 @@ expr_ref sym_expr::accept(expr* e) {
         break;
     }
     case t_char:
+        SASSERT(m.get_sort(e) == m.get_sort(m_t));
         result = m.mk_eq(e, m_t);
         break;
     case t_range: {
@@ -792,8 +793,8 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
         else if (m_util.str.is_empty(e)) {
             continue;
         }
-        else if (m_util.str.is_unit(e)) {
-            seq.push_back(e);
+        else if (m_util.str.is_unit(e, e1)) {
+            seq.push_back(e1);
         }
         else if (m_util.str.is_concat(e, e1, e2)) {
             todo.push_back(e1);
@@ -1420,6 +1421,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
 
 bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
     zstring s;
+    expr* emp = 0;
     for (unsigned i = 0; i < sz; ++i) {
         if (m_util.str.is_unit(es[i])) {
             if (all) return false;
@@ -1434,7 +1436,8 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_ve
             }
         }
         else {
-            lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
+            emp = emp?emp:m_util.str.mk_empty(m().get_sort(es[i]));
+            lhs.push_back(emp);
             rhs.push_back(es[i]);
         }
     }
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index f15e83381..0eac9d316 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -31,6 +31,10 @@ static bool is_hex_digit(char ch, unsigned& d) {
         d = 10 + ch - 'A';
         return true;
     }
+    if ('a' <= ch && ch <= 'f') {
+        d = 10 + ch - 'a';
+        return true;
+    }
     return false;
 }
 
@@ -85,6 +89,7 @@ static bool is_escape_char(char const *& s, unsigned& result) {
         s += 2;
         return true;
     }
+    return false;
 }
 
 zstring::zstring(encoding enc): m_encoding(enc) {}
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index e2b078bcd..74c909c02 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1069,14 +1069,7 @@ namespace datalog {
         func_decl_set::iterator it = rels.begin(), end = rels.end();
         for (; it != end; ++it) {
             func_decl* f = *it;
-            out << "(declare-rel " << f->get_name() << " (";
-            for (unsigned i = 0; i < f->get_arity(); ++i) {                
-                ast_smt2_pp(out, f->get_domain(i), env);
-                if (i + 1 < f->get_arity()) {
-                    out << " ";
-                }
-            }
-            out << "))\n";
+            display_rel_decl(out, f);
         }
 
         if (use_fixedpoint_extensions && do_declare_vars) {
@@ -1120,9 +1113,29 @@ namespace datalog {
         }
         if (use_fixedpoint_extensions) {
             for (unsigned i = 0; i < queries.size(); ++i) {
-                out << "(query ";
-                PP(queries[i].get());                
-                out << ")\n";
+                expr* q = queries[i].get();
+                func_decl_ref fn(m);
+                if (is_query(q)) {
+                    fn = to_app(q)->get_decl();
+                }
+                else {
+                    m_free_vars(q);
+                    m_free_vars.set_default_sort(m.mk_bool_sort());
+                    sort* const* domain = m_free_vars.c_ptr();
+                    expr_ref qfn(m);
+                    expr_ref_vector args(m);
+                    fn = m.mk_fresh_func_decl(symbol("q"), symbol(""), m_free_vars.size(), domain, m.mk_bool_sort());
+                    display_rel_decl(out, fn);
+                    for (unsigned j = 0; j < m_free_vars.size(); ++j) {
+                        args.push_back(m.mk_var(j, m_free_vars[j]));
+                    }
+                    qfn = m.mk_implies(q, m.mk_app(fn, args.size(), args.c_ptr()));
+                    
+                    out << "(assert ";
+                    PP(qfn);
+                    out << ")\n";
+                }
+                out << "(query " << fn->get_name() << ")\n";
             }
         }
         else {
@@ -1139,6 +1152,35 @@ namespace datalog {
         }
     }
 
+    void context::display_rel_decl(std::ostream& out, func_decl* f) {
+        smt2_pp_environment_dbg env(m);
+        out << "(declare-rel " << f->get_name() << " (";
+        for (unsigned i = 0; i < f->get_arity(); ++i) {                
+            ast_smt2_pp(out, f->get_domain(i), env);
+            if (i + 1 < f->get_arity()) {
+                out << " ";
+            }
+        }
+        out << "))\n";
+    }
+
+    bool context::is_query(expr* q) {
+        if (!is_app(q) || !is_predicate(to_app(q)->get_decl())) {
+            return false;
+        }
+        app* a = to_app(q);
+        for (unsigned i = 0; i < a->get_num_args(); ++i) {
+            if (!is_var(a->get_arg(i))) {
+                return false;
+            }
+            var* v = to_var(a->get_arg(i));
+            if (v->get_idx() != i) {
+                return false;
+            }
+        }
+        return true;
+    }
+
 
     void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) {
         //
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index f37169cac..3d8b56beb 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -581,6 +581,9 @@ namespace datalog {
         //undefined and private copy constructor and operator=
         context(const context&);
         context& operator=(const context&);
+
+        bool is_query(expr* e);
+        void display_rel_decl(std::ostream& out, func_decl* f);
     };
 
 };
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 8a40f9d7a..9f7656471 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -847,6 +847,9 @@ namespace smt {
                 setup_AUFLIA(false);
             setup_datatypes();
             setup_bv();
+            setup_dl();
+            setup_seq();
+            setup_card();
             setup_fpa();
             return;
         }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index f4e6d1d57..8c7d24461 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -64,6 +64,34 @@ bool theory_seq::solution_map::is_root(expr* e) const {
     return !m_map.contains(e);
 }
 
+// e1 -> ... -> e2
+// e2 -> e3
+// e1 -> .... -> e3
+
+// e1 -> ... x, e2 -> ... x
+void theory_seq::solution_map::find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds) {
+    dependency* d = 0;
+    std::pair<expr*, dependency*> value(e, d);
+    do {
+        e = value.first;
+        d = m_dm.mk_join(d, value.second);
+        finds.push_back(value);
+    }
+    while (m_map.find(e, value));
+}
+
+bool theory_seq::solution_map::find1(expr* e, expr*& r, dependency*& d) {
+    std::pair<expr*, dependency*> value;    
+    if (m_map.find(e, value)) {
+        d = m_dm.mk_join(d, value.second);
+        r = value.first;
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
 expr* theory_seq::solution_map::find(expr* e, dependency*& d) {
     std::pair<expr*, dependency*> value;
     d = 0;
@@ -183,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() {
@@ -215,21 +243,21 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>check_length_coherence\n";);
         return FC_CONTINUE;
     }
-    if (propagate_automata()) {
-        ++m_stats.m_propagate_automata;
-        TRACE("seq", tout << ">>propagate_automata\n";);
-        return FC_CONTINUE;
-    }
     if (!check_extensionality()) {
         ++m_stats.m_extensionality;
         TRACE("seq", tout << ">>extensionality\n";);
         return FC_CONTINUE;
     }
+    if (propagate_automata()) {
+        ++m_stats.m_propagate_automata;
+        TRACE("seq", tout << ">>propagate_automata\n";);
+        return FC_CONTINUE;
+    }
     if (is_solved()) {
         TRACE("seq", tout << ">>is_solved\n";);
         return FC_DONE;
     }
-
+    TRACE("seq", tout << ">>give_up\n";);
     return FC_GIVEUP;
 }
 
@@ -451,7 +479,7 @@ bool theory_seq::check_length_coherence(expr* e) {
             propagate_is_conc(e, conc);
             assume_equality(tail, emp);
         }
-        if (!get_context().at_base_level()) {
+        else if (!get_context().at_base_level()) {
             m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
         }
         return true;
@@ -501,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));
@@ -573,29 +607,41 @@ bool theory_seq::check_extensionality() {
     unsigned sz = get_num_vars();
     unsigned_vector seqs;
     for (unsigned v = 0; v < sz; ++v) {
-        enode* n = get_enode(v);
-        expr* o1 = n->get_owner();
-        if (n != n->get_root()) {
+        enode* n1 = get_enode(v);
+        expr* o1 = n1->get_owner();
+        if (n1 != n1->get_root()) {
             continue;
         }
-        if (!seqs.empty() && ctx.is_relevant(n) && m_util.is_seq(o1) && ctx.is_shared(n)) {
+        if (!seqs.empty() && ctx.is_relevant(n1) && m_util.is_seq(o1) && ctx.is_shared(n1)) {
             dependency* dep = 0;
             expr_ref e1 = canonize(o1, dep);
             for (unsigned i = 0; i < seqs.size(); ++i) {
                 enode* n2 = get_enode(seqs[i]);
                 expr* o2 = n2->get_owner();
-                if (m_exclude.contains(o1, o2)) {
+                if (m.get_sort(o1) != m.get_sort(o2)) {
+                    continue;
+                }
+                if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) {
                     continue;
                 }
                 expr_ref e2 = canonize(n2->get_owner(), dep);
                 m_lhs.reset(); m_rhs.reset();
                 bool change = false;
-                if (!m_seq_rewrite.reduce_eq(o1, o2, m_lhs, m_rhs, change)) {
+                if (!m_seq_rewrite.reduce_eq(e1, e2, m_lhs, m_rhs, change)) {
                     m_exclude.update(o1, o2);
                     continue;
                 }
-                TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
-                ctx.assume_eq(n, n2);                
+                bool excluded = false;
+                for (unsigned j = 0; !excluded && j < m_lhs.size(); ++j) {
+                    if (m_exclude.contains(m_lhs[j].get(), m_rhs[j].get())) {
+                        excluded = true;
+                    }
+                }
+                if (excluded) {
+                    continue;
+                }
+                TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";);
+                ctx.assume_eq(n1, n2);                
                 return false;
             }
         }
@@ -670,7 +716,7 @@ void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) {
     enode_pair_vector eqs;
     literal_vector lits(_lits);
     linearize(dep, eqs, lits);
-    TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); if (!lits.empty()) tout << "\n"; display_deps(tout, dep); ;);
+    TRACE("seq", display_deps(tout, lits, eqs););
     m_new_propagation = true;
     ctx.set_conflict(
         ctx.mk_justification(
@@ -720,6 +766,7 @@ bool theory_seq::simplify_eq(expr_ref_vector& ls, expr_ref_vector& rs, dependenc
     context& ctx = get_context();
     expr_ref_vector lhs(m), rhs(m);
     bool changed = false;
+    TRACE("seq", tout << ls << " = " << rs << "\n";);
     if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, changed)) {
         // equality is inconsistent.
         TRACE("seq", tout << ls << " != " << rs << "\n";);
@@ -739,9 +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)) {
-            // skip
+            // 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 {
@@ -769,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;
@@ -996,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) {
@@ -1046,7 +1163,7 @@ bool theory_seq::solve_ne(unsigned idx) {
         change = canonize(n.rs(i), rs, deps) || change;
 
         if (!m_seq_rewrite.reduce_eq(ls, rs, lhs, rhs, change)) {
-            TRACE("seq", display_disequation(tout << "reduces to false", n););
+            TRACE("seq", display_disequation(tout << "reduces to false: ", n););
             return true;
         }
         else if (!change) {
@@ -1144,16 +1261,181 @@ bool theory_seq::solve_ne(unsigned idx) {
     if (updated) {
         if (num_undef_lits == 0 && new_ls.empty()) {
             TRACE("seq", tout << "conflict\n";);
+
+            dependency* deps1 = 0;
+            if (explain_eq(n.l(), n.r(), deps1)) {
+                new_lits.reset();
+                new_lits.push_back(~mk_eq(n.l(), n.r(), false));
+                new_deps = deps1;
+                TRACE("seq", tout << "conflict explained\n";);
+            }
             set_conflict(new_deps, new_lits);
             SASSERT(m_new_propagation);
         }
         else {
-            m_nqs.push_back(ne(new_ls, new_rs, new_lits, new_deps));
+            m_nqs.push_back(ne(n.l(), n.r(), new_ls, new_rs, new_lits, new_deps));
         }
     }
     return updated;
 }
 
+theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
+    cell* c = alloc(cell, p, e, d);
+    m_all_cells.push_back(c);
+    return c;
+}
+
+void theory_seq::unfold(cell* c, ptr_vector<cell>& cons) {
+    dependency* dep = 0;
+    expr* a, *e1, *e2;
+    if (m_rep.find1(c->m_expr, a, dep)) {
+        cell* c1 = mk_cell(c, a, m_dm.mk_join(dep, c->m_dep));
+        unfold(c1, cons);
+    }
+    else if (m_util.str.is_concat(c->m_expr, e1, e2)) {
+        cell* c1 = mk_cell(c, e1, c->m_dep);
+        cell* c2 = mk_cell(0, e2, 0);
+        unfold(c1, cons);
+        unfold(c2, cons);
+    }
+    else {
+        cons.push_back(c);
+    }
+    c->m_last = cons.size()-1;
+} 
+// 
+// a -> a1.a2, a2 -> a3.a4 -> ...
+// b -> b1.b2, b2 -> b3.a4 
+// 
+// e1 
+//
+
+void theory_seq::display_explain(std::ostream& out, unsigned indent, expr* e) {
+    expr* e1, *e2, *a;
+    dependency* dep = 0;
+    smt2_pp_environment_dbg env(m);
+    params_ref p;
+    for (unsigned i = 0; i < indent; ++i) out << " ";
+    ast_smt2_pp(out, e, env, p, indent);
+    out << "\n";
+
+    if (m_rep.find1(e, a, dep)) {
+        display_explain(out, indent + 1, a);
+    }
+    else if (m_util.str.is_concat(e, e1, e2)) {
+        display_explain(out, indent + 1, e1);
+        display_explain(out, indent + 1, e2);        
+    }
+}
+
+bool theory_seq::explain_eq(expr* e1, expr* e2, dependency*& dep) {
+
+    if (e1 == e2) {
+        return true;
+    }
+    expr* a1, *a2;
+    ptr_vector<cell> v1, v2;
+    unsigned cells_sz = m_all_cells.size();
+    cell* c1 = mk_cell(0, e1, 0);
+    cell* c2 = mk_cell(0, e2, 0);
+    unfold(c1, v1);
+    unfold(c2, v2);
+    unsigned i = 0, j = 0;
+    
+    TRACE("seq", 
+          tout << "1:\n";
+          display_explain(tout, 0, e1);
+          tout << "2:\n";
+          display_explain(tout, 0, e2););
+
+    bool result = true;
+    while (i < v1.size() || j < v2.size()) {
+        if (i == v1.size()) {
+            while (j < v2.size() && m_util.str.is_empty(v2[j]->m_expr)) {
+                dep = m_dm.mk_join(dep, v2[j]->m_dep);
+                ++j;
+            }
+            result = j == v2.size();
+            break;
+        }
+        if (j == v2.size()) {
+            while (i < v1.size() && m_util.str.is_empty(v1[i]->m_expr)) {
+                dep = m_dm.mk_join(dep, v1[i]->m_dep);
+                ++i;
+            }
+            result = i == v1.size();
+            break;
+        }
+        cell* c1 = v1[i];
+        cell* c2 = v2[j];
+        e1 = c1->m_expr;
+        e2 = c2->m_expr;
+        if (e1 == e2) {
+            if (c1->m_parent && c2->m_parent && 
+                c1->m_parent->m_expr == c2->m_parent->m_expr) {
+                TRACE("seq", tout << "parent: " << mk_pp(e1, m) << " " << mk_pp(c1->m_parent->m_expr, m) << "\n";);
+                c1 = c1->m_parent;
+                c2 = c2->m_parent;
+                v1[c1->m_last] = c1;
+                i = c1->m_last;
+                v2[c2->m_last] = c2;
+                j = c2->m_last;
+            }
+            else {
+                dep = m_dm.mk_join(dep, c1->m_dep);
+                dep = m_dm.mk_join(dep, c2->m_dep);
+                ++i;
+                ++j;
+            }
+        }
+        else if (m_util.str.is_empty(e1)) {
+            dep = m_dm.mk_join(dep, c1->m_dep);
+            ++i;
+        }
+        else if (m_util.str.is_empty(e2)) {
+            dep = m_dm.mk_join(dep, c2->m_dep);
+            ++j;
+        }
+        else if (m_util.str.is_unit(e1, a1) &&
+                 m_util.str.is_unit(e2, a2)) {
+            if (explain_eq(a1, a2, dep)) {
+                ++i;
+                ++j;
+            }
+            else {
+                result = false;
+                break;
+            }
+        }
+        else {
+            TRACE("seq", tout << "Could not solve " << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";);
+            result = false;
+            break;
+        }
+    }   
+    m_all_cells.resize(cells_sz);
+    return result;
+    
+}
+
+bool theory_seq::explain_empty(expr_ref_vector& es, dependency*& dep) {
+    while (!es.empty()) {
+        expr* e = es.back();
+        if (m_util.str.is_empty(e)) {
+            es.pop_back();
+            continue;
+        }
+        expr* a;
+        if (m_rep.find1(e, a, dep)) {
+            es.pop_back();
+            m_util.str.get_concat(a, es);
+            continue;
+        }
+        TRACE("seq", tout << "Could not set to empty: " << es << "\n";);
+        return false;
+    }
+    return true;
+}
 
 bool theory_seq::simplify_and_solve_eqs() {
     context & ctx = get_context();
@@ -1294,18 +1576,44 @@ 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 << "  (= ";
+        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 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";
+    }
+}
+
 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 {
@@ -1534,6 +1842,9 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     else if (m_util.str.is_contains(e, e1, e2)) {
         result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
     }
+    else if (m_util.str.is_unit(e, e1)) {
+        result = m_util.str.mk_unit(expand(e1, deps));
+    }
     else {
         result = e;
     }
@@ -1954,12 +2265,30 @@ bool theory_seq::get_length(expr* e, rational& val) {
 void theory_seq::add_extract_axiom(expr* e) {
     expr* s, *i, *l;
     VERIFY(m_util.str.is_extract(e, s, i, l));
-    expr_ref x(mk_skolem(m_extract_prefix, s, e), m);
+    if (is_tail(s, i, l)) {
+        add_tail_axiom(e, s);
+        return;
+    }
+    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);
 
     literal i_ge_0    = mk_literal(m_autil.mk_ge(i, zero));
@@ -1967,13 +2296,91 @@ void theory_seq::add_extract_axiom(expr* e) {
     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));
 
-    add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
+//    add_axiom(~i_ge_0, ~i_le_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
+    add_axiom(~i_ge_0, ~i_le_ls, mk_seq_eq(xey, s));
     add_axiom(~i_ge_0, ~i_le_ls, mk_eq(lx, i, false));
     add_axiom(~i_ge_0, ~i_le_ls, ~l_ge_zero, ~li_ge_ls, mk_eq(le, l, false));
     add_axiom(~i_ge_0, ~i_le_ls, li_ge_ls, mk_eq(le, mk_sub(ls, i), false));
     add_axiom(~i_ge_0, ~i_le_ls, l_ge_zero, mk_eq(le, zero, false));
 }
 
+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, 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) {
+    rational i1;
+    if (!m_autil.is_numeral(i, i1) || !i1.is_one()) {
+        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_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)
 
@@ -1983,14 +2390,14 @@ void theory_seq::add_extract_axiom(expr* e) {
 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));
@@ -2057,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) {
@@ -2116,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);
@@ -2128,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 7183b2950..3f636347d 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -81,6 +81,8 @@ namespace smt {
             bool  find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); }
             expr* find(expr* e, dependency*& d);
             expr* find(expr* e);
+            bool  find1(expr* a, expr*& b, dependency*& dep);
+            void  find_rec(expr* e, svector<std::pair<expr*, dependency*> >& finds);
             bool  is_root(expr* e) const;
             void  cache(expr* e, expr* r, dependency* d);
             void  reset_cache() { m_cache.reset(); }
@@ -142,31 +144,35 @@ namespace smt {
             return eq(m_eq_id++, ls, rs, dep);
         }        
 
-        class ne {            
-            vector<expr_ref_vector>  m_lhs;
-            vector<expr_ref_vector>  m_rhs;
+        class ne {      
+            expr_ref                 m_l, m_r;
+            vector<expr_ref_vector>  m_lhs, m_rhs;
             literal_vector           m_lits;
             dependency*              m_dep;
         public:
             ne(expr_ref const& l, expr_ref const& r, dependency* dep):
-                m_dep(dep) {
-                expr_ref_vector ls(l.get_manager()); ls.push_back(l);
-                expr_ref_vector rs(r.get_manager()); rs.push_back(r);
+                m_l(l), m_r(r), m_dep(dep) {
+                    expr_ref_vector ls(l.get_manager()); ls.push_back(l);
+                    expr_ref_vector rs(r.get_manager()); rs.push_back(r);
                     m_lhs.push_back(ls);
                     m_rhs.push_back(rs);
                 }
 
-            ne(vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
+            ne(expr_ref const& _l, expr_ref const& _r, vector<expr_ref_vector> const& l, vector<expr_ref_vector> const& r, literal_vector const& lits, dependency* dep):
+                m_l(_l), m_r(_r),
                 m_lhs(l),
                 m_rhs(r),
                 m_lits(lits),
                 m_dep(dep) {}
 
             ne(ne const& other): 
+                m_l(other.m_l), m_r(other.m_r),
                 m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_lits(other.m_lits), m_dep(other.m_dep) {}
 
             ne& operator=(ne const& other) { 
                 if (this != &other) {
+                    m_l = other.m_l;
+                    m_r = other.m_r;
                     m_lhs.reset();  m_lhs.append(other.m_lhs);
                     m_rhs.reset();  m_rhs.append(other.m_rhs); 
                     m_lits.reset(); m_lits.append(other.m_lits); 
@@ -181,6 +187,8 @@ namespace smt {
             literal_vector const& lits() const { return m_lits; }
             literal lits(unsigned i) const { return m_lits[i]; }
             dependency* dep() const { return m_dep; }
+            expr_ref const& l() const { return m_l; }
+            expr_ref const& r() const { return m_r; }
         };
 
         class apply {
@@ -268,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;
 
@@ -326,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()); }
@@ -334,12 +345,27 @@ namespace smt {
         bool solve_nqs(unsigned i);
         bool solve_ne(unsigned i);
 
+        struct cell {
+            cell*       m_parent;
+            expr*       m_expr;
+            dependency* m_dep;
+            unsigned    m_last;
+            cell(cell* p, expr* e, dependency* d): m_parent(p), m_expr(e), m_dep(d), m_last(0) {}
+        };
+        scoped_ptr_vector<cell> m_all_cells;
+        cell* mk_cell(cell* p, expr* e, dependency* d);
+        void unfold(cell* c, ptr_vector<cell>& cons);
+        void display_explain(std::ostream& out, unsigned indent, expr* e);
+        bool explain_eq(expr* e1, expr* e2, dependency*& dep);
+        bool explain_empty(expr_ref_vector& es, dependency*& dep);
+
         // asserting consequences
         void linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const;
         void propagate_lit(dependency* dep, literal lit) { propagate_lit(dep, 0, 0, lit); }
         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;
@@ -357,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);
@@ -376,6 +403,15 @@ namespace smt {
         void add_replace_axiom(expr* e);
         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);
@@ -445,6 +481,7 @@ namespace smt {
         void display_disequations(std::ostream& out) const;
         void display_disequation(std::ostream& out, ne const& e) const;
         void display_deps(std::ostream& out, dependency* deps) const;
+        void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
     public:
         theory_seq(ast_manager& m);
         virtual ~theory_seq();
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 08463cf20..338a4a7da 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -190,14 +190,14 @@ public:
     }
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
-        m_check_sat_executed  = true;
-        
+        m_check_sat_executed  = true;        
+        m_use_solver1_results = false;
+
         if (get_num_assumptions() != 0 ||            
             num_assumptions > 0 || // assumptions were provided
             m_ignore_solver1)  {
             // must use incremental solver
             switch_inc_mode();
-            m_use_solver1_results = false;
             return m_solver2->check_sat(num_assumptions, assumptions);
         }
         
@@ -206,7 +206,6 @@ public:
                 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);            
                 lbool r = m_solver2->check_sat(0, 0);
                 if (r != l_undef || !use_solver1_when_undef()) {
-                    m_use_solver1_results = false;
                     return r;
                 }
             }
@@ -219,7 +218,6 @@ public:
                     r = m_solver2->check_sat(0, 0);
                 }
                 if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
-                    m_use_solver1_results = false;
                     return r;
                 }
                 if (eh.m_canceled) {
@@ -227,7 +225,6 @@ public:
                 }
             }
             IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
-
         }
         
         IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 5bcf5eae3..37ad9c73c 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -75,7 +75,7 @@ class ufbv_rewriter_tactic : public tactic {
         void updt_params(params_ref const & p) {
         }
     };
-    
+
     imp *      m_imp;
     params_ref m_params;
 
@@ -88,7 +88,7 @@ public:
     virtual tactic * translate(ast_manager & m) {
         return alloc(ufbv_rewriter_tactic, m, m_params);
     }
-        
+
     virtual ~ufbv_rewriter_tactic() {
         dealloc(m_imp);
     }
@@ -103,19 +103,19 @@ public:
         insert_produce_models(r);
         insert_produce_proofs(r);
     }
-    
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            model_converter_ref & mc, 
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
                             proof_converter_ref & pc,
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-    
+
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
         imp * d = alloc(imp, m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }
 
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.h b/src/tactic/ufbv/ufbv_rewriter_tactic.h
index 85cffee54..78e34bae2 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.h
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("ufbv-rewriter",  "Applies UFBV-specific rewriting rules, mainly demodulation.", "mk_quasi_macros_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 34aee9d6e..b6831faa7 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -46,11 +46,6 @@ public:
     out_of_memory_error();
 };
 
-class exceeded_memory_allocations : public z3_error {
-public:
-    exceeded_memory_allocations();
-};
-
 class memory {
 public:
     static bool is_out_of_memory();