diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
index 921cace75..14bcebf46 100644
--- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt
+++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
@@ -20,6 +20,8 @@ z3_add_component(rewriter
     seq_rewriter.cpp
     th_rewriter.cpp
     var_subst.cpp
+    bv_trailing.cpp
+    mk_extract_proc.cpp
   COMPONENT_DEPENDENCIES
     ast
     automata
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 5c7a819da..7c846cc99 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4538,6 +4538,9 @@ extern "C" {
        If \c model_completion is Z3_TRUE, then Z3 will assign an interpretation for any constant or function that does
        not have an interpretation in \c m. These constants and functions were essentially don't cares.
 
+       If \c model_completion is Z3_FALSE, then Z3 will not assign interpretations to constants for functions that do
+       not have interpretations in \c m. Evaluation behaves as the identify function in this case.
+
        The evaluation may fail for the following reasons:
 
        - \c t contains a quantifier.
@@ -4547,6 +4550,8 @@ extern "C" {
 
        - \c t is type incorrect.
 
+       - \c Z3_interrupt was invoked during evaluation.
+
        def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
     */
     Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v);
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 7322977a0..def05f014 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -22,45 +22,13 @@ Notes:
 #include"ast_smt2_pp.h"
 
 
-mk_extract_proc::mk_extract_proc(bv_util & u):
-    m_util(u),
-    m_high(0),
-    m_low(UINT_MAX),
-    m_domain(0),
-    m_f_cached(0) {
-}
-
-mk_extract_proc::~mk_extract_proc() {
-    if (m_f_cached) {
-        // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
-        ast_manager & m = m_util.get_manager();
-        m.dec_ref(m_f_cached);
-    }
-}
-
-app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
-    ast_manager & m = m_util.get_manager();
-    sort * s = m.get_sort(arg);
-    if (m_low == low && m_high == high && m_domain == s)
-        return m.mk_app(m_f_cached, arg);
-    // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
-    if (m_f_cached)
-        m.dec_ref(m_f_cached);
-    app * r    = to_app(m_util.mk_extract(high, low, arg));
-    m_high     = high;
-    m_low      = low;
-    m_domain   = s;
-    m_f_cached = r->get_decl();
-    m.inc_ref(m_f_cached);
-    return r;
-}
-
 void bv_rewriter::updt_local_params(params_ref const & _p) {
     bv_rewriter_params p(_p);
     m_hi_div0 = p.hi_div0();
     m_elim_sign_ext = p.elim_sign_ext();
     m_mul2concat = p.mul2concat();
     m_bit2bool = p.bit2bool();
+    m_trailing = p.bv_trailing();
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
     m_udiv2mul = p.udiv2mul();
@@ -2124,6 +2092,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
+    if (m_trailing) {
+        st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
+        m_rm_trailing.reset_cache(1 << 12);
+        if (st != BR_FAILED) {
+            TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
+            return st;
+        }
+    }
+
     st = mk_mul_eq(lhs, rhs, result);
     if (st != BR_FAILED) {
         TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);
@@ -2187,6 +2164,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     return BR_FAILED;
 }
 
+
 br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
     if (m_mkbv2num) {
         unsigned i;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index f01743ca9..7135c52ba 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -22,18 +22,8 @@ Notes:
 #include"poly_rewriter.h"
 #include"bv_decl_plugin.h"
 #include"arith_decl_plugin.h"
-
-class mk_extract_proc {
-    bv_util &     m_util;
-    unsigned      m_high;
-    unsigned      m_low;
-    sort *        m_domain;
-    func_decl *   m_f_cached;
-public:
-    mk_extract_proc(bv_util & u);
-    ~mk_extract_proc();
-    app * operator()(unsigned high, unsigned low, expr * arg);
-};
+#include"mk_extract_proc.h"
+#include"bv_trailing.h"
 
 class bv_rewriter_core {
 protected:
@@ -58,6 +48,7 @@ public:
 
 class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     mk_extract_proc m_mk_extract;
+    bv_trailing     m_rm_trailing;
     arith_util m_autil;
     bool       m_hi_div0;
     bool       m_elim_sign_ext;
@@ -69,6 +60,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_udiv2mul;
     bool       m_bvnot2arith;
     bool       m_bv_sort_ac;
+    bool       m_trailing;
 
     bool is_zero_bit(expr * x, unsigned idx);
 
@@ -148,6 +140,7 @@ public:
     bv_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         poly_rewriter<bv_rewriter_core>(m, p),
         m_mk_extract(m_util),
+        m_rm_trailing(m_mk_extract),
         m_autil(m) {
         updt_local_params(p);
     }
diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg
index 5feece753..0f0163fb1 100644
--- a/src/ast/rewriter/bv_rewriter_params.pyg
+++ b/src/ast/rewriter/bv_rewriter_params.pyg
@@ -9,5 +9,6 @@ def_module_params(module_name='rewriter',
                           ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
                           ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
                           ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
-                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators")
+                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
+                          ("bv_trailing", BOOL, False, "lean removal of trailing zeros")
                           ))
diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp
new file mode 100644
index 000000000..9a5c0107d
--- /dev/null
+++ b/src/ast/rewriter/bv_trailing.cpp
@@ -0,0 +1,404 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  bv_trailing.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"bv_trailing.h"
+#include"bv_decl_plugin.h"
+#include"ast_smt2_pp.h"
+
+// The analyzer gives up analysis after going TRAILING_DEPTH deep.
+// This number shouldn't be too big.
+#define  TRAILING_DEPTH 5
+
+struct bv_trailing::imp {
+    typedef rational numeral;
+    typedef obj_map<expr, std::pair<unsigned,unsigned> > map;
+    mk_extract_proc&     m_mk_extract;
+    bv_util&             m_util;
+    ast_manager&         m_m;
+
+    // keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level
+    map*                 m_count_cache[TRAILING_DEPTH + 1];
+
+    imp(mk_extract_proc& mk_extract)
+        : m_mk_extract(mk_extract)
+        , m_util(mk_extract.bvutil())
+        , m_m(mk_extract.m()) {
+            for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
+                m_count_cache[i] = NULL;
+    }
+
+    virtual ~imp() {
+        reset_cache(0);
+    }
+
+    ast_manager & m() const { return m_util.get_manager(); }
+
+    br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) {
+        TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m()) << "\n=\n" << mk_ismt2_pp(e2, m()) << "\n";);
+        SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2));
+        SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2));
+        unsigned max1, min1, max2, min2;
+        count_trailing(e1, min1, max1, TRAILING_DEPTH);
+        count_trailing(e2, min2, max2, TRAILING_DEPTH);
+        if (min1 > max2 || min2 > max1) { // bounds have empty intersection
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds
+        if (min == 0) { // nothing to remove
+            result = m().mk_eq(e1, e2);
+            return BR_FAILED;
+        }
+        const unsigned sz  = m_util.get_bv_size(e1);
+        if (min == sz) { // everything removed, unlikely but we check anyhow for safety
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        expr_ref out1(m());
+        expr_ref out2(m());
+        const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
+        const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
+        SASSERT(rm1 == min && rm2 == min);
+        const bool are_eq = m().are_equal(out1, out2);
+        result = are_eq ? m().mk_true() : m().mk_eq(out1, out2);
+        return are_eq ? BR_DONE : BR_REWRITE2;
+    }
+
+    // This routine needs to be implemented carefully so that whenever it
+    // returns a lower bound on trailing zeros min, the routine remove_trailing
+    // must be capable of removing at least that many zeros from the expression.
+    void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) {
+        SASSERT(e && m_util.is_bv(e));
+        if (is_cached(depth, e, min, max)) return;
+        count_trailing_core(e, min, max, depth);
+        TRACE("bv-trailing", tout << mk_ismt2_pp(e, m()) << "\n:" << min << " - " << max << "\n";);
+        SASSERT(min <= max);
+        SASSERT(max <= m_util.get_bv_size(e));
+        cache(depth, e, min, max);  // store result into the cache
+    }
+
+    unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) {
+        const unsigned retv = remove_trailing_core(e, n, result, depth);
+        CTRACE("bv-trailing", result.get(),  tout << mk_ismt2_pp(e, m()) << "\n--->\n" <<  mk_ismt2_pp(result.get(), m())  << "\n";);
+        CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m()) << "\n---> [EMPTY]\n";);
+        return retv;
+    }
+
+    // Assumes that count_trailing gives me a lower bound that we can also remove from each summand.
+    unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_bv_add(a));
+        const unsigned num  = a->get_num_args();
+        if (depth <= 1) {
+            result = a;
+            return 0;
+        }
+        unsigned min, max;
+        count_trailing(a, min, max, depth); // caching is important here
+        const unsigned to_rm = std::min(min, n);
+        if (to_rm == 0) {
+            result = a;
+            return 0;
+        }
+
+        const unsigned sz = m_util.get_bv_size(a);
+
+        if (to_rm == sz) {
+            result = NULL;
+            return sz;
+        }
+
+        expr_ref_vector new_args(m());
+        expr_ref tmp(m());
+        for (unsigned i = 0; i < num; ++i) {
+            expr * const curr = a->get_arg(i);
+            const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1);
+            new_args.push_back(tmp);
+            SASSERT(crm == to_rm);
+        }
+        result = m().mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
+        return to_rm;
+    }
+
+    unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_bv_mul(a));
+        const unsigned num  = a->get_num_args();
+        if (depth <= 1 || !num) {
+            result = a;
+            return 0;
+        }
+        expr_ref tmp(m());
+        expr * const coefficient = a->get_arg(0);
+        const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1);
+        SASSERT(retv <= n);
+        if (retv == 0) {
+            result = a;
+            return 0;
+        }
+        expr_ref_vector new_args(m());
+        numeral c_val;
+        unsigned c_sz;
+        if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
+            new_args.push_back(tmp);
+        const unsigned sz = m_util.get_bv_size(coefficient);
+        const unsigned new_sz = sz - retv;
+
+        if (!new_sz) {
+            result = NULL;
+            return retv;
+        }
+
+        SASSERT(m_util.get_bv_size(tmp) == new_sz);
+        for (unsigned i = 1; i < num; i++) {
+            expr * const curr = a->get_arg(i);
+            new_args.push_back(m_mk_extract(new_sz - 1, 0, curr));
+        }
+        switch (new_args.size()) {
+        case 0: result = m_util.mk_numeral(1, new_sz); break;
+        case 1: result = new_args.get(0); break;
+        default: result = m().mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
+        }
+        return retv;
+    }
+
+    unsigned remove_trailing_concat(app * a, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_concat(a));
+        if (depth <= 1) {
+            result = a;
+            return 0;
+        }
+        const unsigned num  = a->get_num_args();
+        unsigned retv = 0;
+        unsigned i = num;
+        expr_ref new_last(NULL, m());
+        while (i && retv < n) {
+            i--;
+            expr * const curr = a->get_arg(i);
+            const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
+            const unsigned curr_sz = m_util.get_bv_size(curr);
+            retv += cur_rm;
+            if (cur_rm < curr_sz) break;
+        }
+        if (retv == 0) {
+            result = a;
+            return 0;
+        }
+
+        if (!i) {// all args eaten completely
+            SASSERT(new_last.get() == NULL);
+            SASSERT(retv == m_util.get_bv_size(a));
+            result = NULL;
+            return retv;
+        }
+
+        expr_ref_vector new_args(m());
+        for (size_t j=0; j<i;++j)
+            new_args.push_back(a->get_arg(j));
+        if (new_last.get()) new_args.push_back(new_last);
+        result = new_args.size() == 1 ? new_args.get(0)
+                                      : m_util.mk_concat(new_args.size(), new_args.c_ptr());
+        return retv;
+    }
+
+    unsigned remove_trailing(size_t max_rm, numeral& a) {
+        numeral two(2);
+        unsigned retv = 0;
+        while (max_rm && a.is_even()) {
+            div(a, two, a);
+            ++retv;
+            --max_rm;
+        }
+        return retv;
+    }
+
+    unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) {
+        SASSERT(m_util.is_bv(e));
+        if (!depth || !n) return 0;
+        unsigned sz;
+        unsigned retv = 0;
+        numeral e_val;
+        if (m_util.is_numeral(e, e_val, sz)) {
+            retv = remove_trailing(n, e_val);
+            const unsigned new_sz = sz - retv;
+            result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
+            return retv;
+        }
+        if (m_util.is_bv_mul(e))
+            return remove_trailing_mul(to_app(e), n, result, depth);
+        if (m_util.is_bv_add(e))
+            return remove_trailing_add(to_app(e), n, result, depth);
+        if (m_util.is_concat(e))
+            return remove_trailing_concat(to_app(e), n, result, depth);
+        return 0;
+    }
+
+
+    void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) {
+        if (depth <= 1) {
+            min = 0;
+            max = m_util.get_bv_size(a);
+        }
+        max = min = 0; // treat empty concat as the empty string
+        unsigned num = a->get_num_args();
+        bool update_min = true;
+        bool update_max = true;
+        unsigned tmp_min, tmp_max;
+        while (num-- && update_max) {
+            expr * const curr = a->get_arg(num);
+            const unsigned curr_sz = m_util.get_bv_size(curr);
+            count_trailing(curr, tmp_min, tmp_max, depth - 1);
+            SASSERT(curr_sz != tmp_min || curr_sz == tmp_max);
+            max += tmp_max;
+            if (update_min) min += tmp_min;
+            //  continue updating only if eaten away completely
+            update_min &= curr_sz == tmp_min;
+            update_max &= curr_sz == tmp_max;
+        }
+    }
+
+    void count_trailing_add(app * a, unsigned& min, unsigned& max, unsigned depth) {
+        if (depth <= 1) {
+            min = 0;
+            max = m_util.get_bv_size(a);
+        }
+        const unsigned num = a->get_num_args();
+        const unsigned sz = m_util.get_bv_size(a);
+        min = max = sz; // treat empty addition as 0
+        unsigned tmp_min;
+        unsigned tmp_max;
+        bool known_parity = true;
+        bool is_odd = false;
+        for (unsigned i = 0; i < num; ++i) {
+            expr * const curr = a->get_arg(i);
+            count_trailing(curr, tmp_min, tmp_max, depth - 1);
+            min = std::min(min, tmp_min);
+            known_parity = known_parity && (!tmp_max || tmp_min);
+            if (known_parity && !tmp_max) is_odd = !is_odd;
+            if (!known_parity && !min) break; // no more information can be gained
+        }
+        max = known_parity && is_odd ? 0 : sz; // max is known if parity is 1
+    }
+
+    void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) {
+        if (depth <= 1) {
+            min = 0;
+            max = m_util.get_bv_size(a);
+        }
+
+        const unsigned num = a->get_num_args();
+        if (!num) {
+            max = min = 0; // treat empty multiplication as 1
+            return;
+        }
+        // assume that numerals are pushed in the front, count only for the first element
+        expr * const curr = a->get_arg(0);
+        unsigned tmp_max;
+        count_trailing(curr, min, tmp_max, depth - 1);
+        max = num == 1 ? tmp_max : m_util.get_bv_size(a);
+        return;
+    }
+
+    void count_trailing_core(expr * e, unsigned& min, unsigned& max, unsigned depth) {
+        if (!depth) {
+            min = 0;
+            max = m_util.get_bv_size(e);
+            return;
+        }
+        unsigned sz;
+        numeral e_val;
+        if (m_util.is_numeral(e, e_val, sz)) {
+            min = max = 0;
+            numeral two(2);
+            while (sz-- && e_val.is_even()) {
+                ++max;
+                ++min;
+                div(e_val, two, e_val);
+            }
+            return;
+        }
+        if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth);
+        else if (m_util.is_bv_add(e)) count_trailing_add(to_app(e), min, max, depth);
+        else if (m_util.is_concat(e)) count_trailing_concat(to_app(e), min, max, depth);
+        else {
+            min = 0;
+            max = m_util.get_bv_size(e);
+        }
+    }
+
+    void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
+        SASSERT(depth <= TRAILING_DEPTH);
+        if (depth == 0) return;
+        if (m_count_cache[depth] == NULL)
+            m_count_cache[depth] = alloc(map);
+        m().inc_ref(e);
+        m_count_cache[depth]->insert(e, std::make_pair(min, max));
+        TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
+    }
+
+    bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) {
+        SASSERT(depth <= TRAILING_DEPTH);
+        if (depth == 0) {
+            min = 0;
+            max = m_util.get_bv_size(e);
+            return true;
+        }
+        if (m_count_cache[depth] == NULL)
+            return false;
+        const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e);
+        if (oe == NULL) return false;
+        min = oe->get_data().m_value.first;
+        max = oe->get_data().m_value.second;
+        TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m()) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
+        return true;
+    }
+
+    void reset_cache(unsigned condition) {
+        SASSERT(m_count_cache[0] == NULL);
+        for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
+            if (m_count_cache[i] == NULL) continue;
+            if (m_count_cache[i]->size() < condition) continue;
+            map::iterator it = m_count_cache[i]->begin();
+            map::iterator end = m_count_cache[i]->end();
+            for (; it != end; ++it) m().dec_ref(it->m_key);
+            dealloc(m_count_cache[i]);
+            m_count_cache[i] = NULL;
+        }
+    }
+
+};
+
+bv_trailing::bv_trailing(mk_extract_proc& mk_extract) {
+    m_imp = alloc(imp, mk_extract);
+}
+
+bv_trailing::~bv_trailing() {
+    if (m_imp) dealloc(m_imp);
+}
+
+br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2,  expr_ref& result) {
+    return m_imp->eq_remove_trailing(e1, e2, result);
+}
+
+void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) {
+     m_imp->count_trailing(e, min, max, TRAILING_DEPTH);
+}
+
+unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) {
+    return m_imp->remove_trailing(e, n, result, TRAILING_DEPTH);
+}
+
+void bv_trailing::reset_cache(unsigned condition) {
+    m_imp->reset_cache(condition);
+}
diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h
new file mode 100644
index 000000000..862a1bea6
--- /dev/null
+++ b/src/ast/rewriter/bv_trailing.h
@@ -0,0 +1,46 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  bv_trailing.h
+
+ Abstract:
+
+ A utility to count trailing zeros of an expression.  Treats 2x and x++0 equivalently.
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+ --*/
+#ifndef BV_TRAILING_H_
+#define BV_TRAILING_H_
+#include"ast.h"
+#include"rewriter_types.h"
+#include"mk_extract_proc.h"
+class bv_trailing {
+    public:
+        bv_trailing(mk_extract_proc& ep);
+        virtual ~bv_trailing();
+    public:
+        // Remove trailing zeros from both sides of an equality (might give False).
+        br_status eq_remove_trailing(expr * e1, expr * e2,  expr_ref& result);
+
+        // Gives a lower and upper bound on trailing zeros in e.
+        void count_trailing(expr * e, unsigned& min, unsigned& max);
+
+        // Attempts removing n trailing zeros from e. Returns how many were successfully removed.
+        // We're assuming that it can remove at least as many zeros as min returned by count_training.
+        // Removing the bit-width of e, sets result to NULL.
+        unsigned remove_trailing(expr * e, unsigned n, expr_ref& result);
+
+        // Reset cache(s) if it exceeded size condition.
+        void reset_cache(unsigned condition);
+    protected:
+        struct imp;
+        imp *        m_imp;
+};
+#endif /* BV_TRAILING_H_ */
diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp
new file mode 100644
index 000000000..5f470acd3
--- /dev/null
+++ b/src/ast/rewriter/mk_extract_proc.cpp
@@ -0,0 +1,49 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  mk_extract_proc.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"mk_extract_proc.h"
+mk_extract_proc::mk_extract_proc(bv_util & u):
+    m_util(u),
+    m_high(0),
+    m_low(UINT_MAX),
+    m_domain(0),
+    m_f_cached(0) {
+}
+
+mk_extract_proc::~mk_extract_proc() {
+    if (m_f_cached) {
+        // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
+        ast_manager & m = m_util.get_manager();
+        m.dec_ref(m_f_cached);
+    }
+}
+
+app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) {
+    ast_manager & m = m_util.get_manager();
+    sort * s = m.get_sort(arg);
+    if (m_low == low && m_high == high && m_domain == s)
+        return m.mk_app(m_f_cached, arg);
+    // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain
+    if (m_f_cached)
+        m.dec_ref(m_f_cached);
+    app * r    = to_app(m_util.mk_extract(high, low, arg));
+    m_high     = high;
+    m_low      = low;
+    m_domain   = s;
+    m_f_cached = r->get_decl();
+    m.inc_ref(m_f_cached);
+    return r;
+}
diff --git a/src/ast/rewriter/mk_extract_proc.h b/src/ast/rewriter/mk_extract_proc.h
new file mode 100644
index 000000000..2b242d0f5
--- /dev/null
+++ b/src/ast/rewriter/mk_extract_proc.h
@@ -0,0 +1,34 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  mk_extract_proc.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+ --*/
+#ifndef MK_EXTRACT_PROC_H_
+#define MK_EXTRACT_PROC_H_
+#include"ast.h"
+#include"bv_decl_plugin.h"
+class mk_extract_proc {
+    bv_util &     m_util;
+    unsigned      m_high;
+    unsigned      m_low;
+    sort *        m_domain;
+    func_decl *   m_f_cached;
+public:
+    mk_extract_proc(bv_util & u);
+    ~mk_extract_proc();
+    app * operator()(unsigned high, unsigned low, expr * arg);
+    ast_manager & m() { return m_util.get_manager(); }
+    bv_util & bvutil() { return m_util; }
+};
+#endif /* MK_EXTRACT_PROC_H_ */
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 63bdbd519..962c9660e 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -825,15 +825,17 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
     if (c_at_rhs) {
         c.neg();
         normalize(c);
-        new_rhs_monomials[0] = mk_numeral(c);
-        lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1);
-        rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr());
-    }
-    else {
-        new_lhs_monomials[0] = mk_numeral(c);
-        lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr());
-        rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1);
     }
+    // When recreating the lhs and rhs also insert coefficient on the appropriate side.
+    // Ignore coefficient if it's 0 and there are no other summands.
+    const bool insert_c_lhs = !c_at_rhs && (new_lhs_monomials.size() == 1 || !c.is_zero());
+    const bool insert_c_rhs =  c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero());
+    const unsigned lhs_offset = insert_c_lhs ? 0 : 1;
+    const unsigned rhs_offset = insert_c_rhs ? 0 : 1;
+    new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL;
+    new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL;
+    lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
+    rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
     return BR_DONE;
 }
 
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index f4a890a2c..3111f2b6c 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include"fpa_rewriter.h"
 #include"rewriter_def.h"
 #include"cooperate.h"
+#include"ast_pp.h"
 
 
 struct evaluator_cfg : public default_rewriter_cfg {
@@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     pb_rewriter                     m_pb_rw;
     fpa_rewriter                    m_f_rw;
     seq_rewriter                    m_seq_rw;
+    array_util                      m_ar;
     unsigned long long              m_max_memory;
     unsigned                        m_max_steps;
     bool                            m_model_completion;
@@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_dt_rw(m),
         m_pb_rw(m),
         m_f_rw(m),
-        m_seq_rw(m) {
+        m_seq_rw(m),
+        m_ar(m) {
         bool flat = true;
         m_b_rw.set_flat(flat);
         m_a_rw.set_flat(flat);
@@ -116,6 +119,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             if (val != 0) {
                 result = val;
                 return BR_DONE;
+//                return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
             }
 
             if (m_model_completion) {
@@ -146,6 +150,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     st = m_f_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
+                else if (fid == m_ar_rw.get_fid())
+                    st = mk_array_eq(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
             }
@@ -182,6 +188,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return st;
     }
 
+
     bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
 
 #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
@@ -230,6 +237,85 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
     bool cache_results() const { return m_cache; }
 
+
+    br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
+        if (a == b) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        vector<expr_ref_vector> stores;
+        expr_ref else1(m()), else2(m());
+        if (extract_array_func_interp(a, stores, else1) &&
+            extract_array_func_interp(b, stores, else2)) {
+            expr_ref_vector conj(m()), args1(m()), args2(m());
+            conj.push_back(m().mk_eq(else1, else2));
+            args1.push_back(a);
+            args2.push_back(b);
+            for (unsigned i = 0; i < stores.size(); ++i) {
+                args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr());
+                args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr());
+                expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr());
+                expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr());
+                conj.push_back(m().mk_eq(s1, s2));
+            }
+            result = m().mk_and(conj.size(), conj.c_ptr());
+            return BR_REWRITE_FULL;
+        }
+        return BR_FAILED;
+    }
+
+    bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case) {
+        SASSERT(m_ar.is_array(a));
+    
+        while (m_ar.is_store(a)) {
+            expr_ref_vector store(m());
+            store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
+            stores.push_back(store);
+            a = to_app(a)->get_arg(0);
+        }
+    
+        if (m_ar.is_const(a)) {
+            else_case = to_app(a)->get_arg(0);
+            return true;
+        }
+    
+        if (m_ar.is_as_array(a)) {
+            func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
+            func_interp* g = m_model.get_func_interp(f);
+            unsigned sz = g->num_entries();
+            unsigned arity = f->get_arity();
+            for (unsigned i = 0; i < sz; ++i) {
+                expr_ref_vector store(m());
+                func_entry const* fe = g->get_entry(i);
+                store.append(arity, fe->get_args());
+                store.push_back(fe->get_result());
+                for (unsigned j = 0; j < store.size(); ++j) {
+                    if (!is_ground(store[j].get())) {
+                        TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";);
+                        return false;
+                    }
+                }
+                stores.push_back(store);
+            }        
+            else_case = g->get_else();
+            if (!else_case) {
+                TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";);
+                return false;
+            }
+            if (!is_ground(else_case)) {
+                TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";);
+                return false;
+            }
+            TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
+            return true;
+        }
+        TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";);
+        
+        return false;
+    }
+
+
+
 };
 
 template class rewriter_tpl<evaluator_cfg>;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index db62febbd..b200524e7 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -401,7 +401,7 @@ namespace sat {
         literal_vector::iterator l_it = m_bs_ls.begin();
         for (; it != end; ++it, ++l_it) {
             clause & c2 = *(*it);
-            if (*l_it == null_literal) {
+            if (!c2.was_removed() && *l_it == null_literal) {
                 // c2 was subsumed
                 if (c1.is_learned() && !c2.is_learned())
                     c1.unset_learned();
diff --git a/src/smt/smt_farkas_util.cpp b/src/smt/smt_farkas_util.cpp
index c1a303299..c5ff42e3e 100644
--- a/src/smt/smt_farkas_util.cpp
+++ b/src/smt/smt_farkas_util.cpp
@@ -62,7 +62,7 @@ namespace smt {
 
     app* farkas_util::mk_ge(expr* e1, expr* e2) {
         mk_coerce(e1, e2);
-        return a.mk_gt(e1, e2);
+        return a.mk_ge(e1, e2);
     }
 
     app* farkas_util::mk_gt(expr* e1, expr* e2) {
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 6ebbbbf0d..8a83b93bd 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3212,7 +3212,8 @@ namespace smt {
     template<typename Ext>
     bool theory_arith<Ext>::get_value(enode * n, expr_ref & r) {
         theory_var v = n->get_th_var(get_id());
-        return v != null_theory_var && to_expr(get_value(v), is_int(v), r);
+        inf_numeral val;
+        return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r);
     }
 
     template<typename Ext>
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index adff16c35..7703f70aa 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -15,7 +15,6 @@ Author:
 
 Revision History:
 
-    // Use instead reference counts for dependencies to GC?
 
 --*/
 
@@ -258,7 +257,7 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>fixed_length\n";);
         return FC_CONTINUE;
     }
-    if (branch_variable()) {
+    if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() ||  branch_variable()) {
         ++m_stats.m_branch_variable;
         TRACE("seq", tout << ">>branch_variable\n";);
         return FC_CONTINUE;
@@ -291,8 +290,7 @@ final_check_status theory_seq::final_check_eh() {
     return FC_GIVEUP;
 }
 
-
-bool theory_seq::branch_variable() {
+bool theory_seq::reduce_length_eq() {
     context& ctx = get_context();
     unsigned sz = m_eqs.size();
     int start = ctx.get_random_value();
@@ -304,25 +302,344 @@ bool theory_seq::branch_variable() {
             return true;
         }
     }
+    return false;
+}
+
+bool theory_seq::branch_binary_variable() {
+    unsigned sz = m_eqs.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        eq const& e = m_eqs[i];
+        if (branch_binary_variable(e)) {
+            return true;
+        }
+    }
+    return false;
+}
+
+bool theory_seq::branch_binary_variable(eq const& e) {
+    if (is_complex(e)) {
+        return false;
+    }
+    ptr_vector<expr> xs, ys;
+    expr* x, *y;
+    bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y);
+    if (!is_binary) {
+        is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y);
+    }
+    if (!is_binary) {
+        return false;
+    }
+    if (x == y) {
+        return false;
+    }
+        
+    // Equation is of the form x ++ xs = ys ++ y
+    // where xs, ys are units.
+    // x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs 
+    
+    rational lenX, lenY;
+    context& ctx = get_context();
+    if (branch_variable(e)) {
+        return true;
+    }
+    if (!get_length(x, lenX)) {
+        enforce_length(ensure_enode(x));
+        return true;
+    }
+    if (!get_length(y, lenY)) {
+        enforce_length(ensure_enode(y));
+        return true;
+    }
+    if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
+        // |x| - |y| = |ys| - |xs|
+        expr_ref a(mk_sub(m_util.str.mk_length(x), m_util.str.mk_length(y)), m);
+        expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m);
+        propagate_lit(e.dep(), 0, 0, mk_eq(a, b, false));
+        return true;
+    }
+    if (lenX <= rational(ys.size())) {
+        expr_ref_vector Ys(m);
+        Ys.append(ys.size(), ys.c_ptr());
+        branch_unit_variable(e.dep(), x, Ys);
+        return true;
+    }
+    expr_ref le(m_autil.mk_le(m_util.str.mk_length(x), m_autil.mk_int(ys.size())), m);
+    literal lit = mk_literal(le);
+    if (l_false == ctx.get_assignment(lit)) {
+        // |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs
+        expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m);
+        expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m);
+        ys.push_back(Y1);
+        expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m);
+        expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m);
+        expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
+        literal_vector lits;
+        lits.push_back(~lit);
+        dependency* dep = e.dep();
+        propagate_eq(dep, lits, x, ysY1, true);
+        propagate_eq(dep, lits, y, Y1Y2, true);
+        propagate_eq(dep, lits, Y2, xsE, true);
+    }
+    else {
+        ctx.mark_as_relevant(lit);
+    }
+    return true;
+}
+
+bool theory_seq::branch_unit_variable() {
+    unsigned sz = m_eqs.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        eq const& e = m_eqs[i];
+        if (is_unit_eq(e.ls(), e.rs())) {
+            branch_unit_variable(e.dep(), e.ls()[0], e.rs());
+            return true;
+        }
+        else if (is_unit_eq(e.rs(), e.ls())) {
+            branch_unit_variable(e.dep(), e.rs()[0], e.ls());
+            return true;
+        }
+    }
+    return false;
+}
+
+/**
+  \brief ls := X... == rs := abcdef
+*/
+bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) {
+    if (ls.empty() || !is_var(ls[0])) {
+        return false;
+    }
+    for (unsigned i = 0; i < rs.size(); ++i) {
+        if (!m_util.str.is_unit(rs[i])) {
+            return false;
+        }
+    }
+    return true;
+}
+
+void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) {
+    SASSERT(is_var(X));
+    context& ctx = get_context();
+    rational lenX;
+    if (!get_length(X, lenX)) {
+        enforce_length(ensure_enode(X));
+        return;
+    }
+    if (lenX > rational(units.size())) {
+        expr_ref le(m_autil.mk_le(m_util.str.mk_length(X), m_autil.mk_int(units.size())), m);
+        propagate_lit(dep, 0, 0, mk_literal(le));
+        return;
+    }
+    SASSERT(lenX.is_unsigned());
+    unsigned lX = lenX.get_unsigned();
+    if (lX == 0) {
+        set_empty(X);
+    }
+    else {
+        literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false);
+        if (l_true == ctx.get_assignment(lit)) {
+            expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m);
+            literal_vector lits;
+            lits.push_back(lit);
+            propagate_eq(dep, lits, X, R, true);
+        }
+        else {
+            ctx.mark_as_relevant(lit);
+            ctx.force_phase(lit);
+        }
+    }
+}
+
+bool theory_seq::branch_variable_mb() {
+    context& ctx = get_context();
+    bool change = false;
+    for (unsigned i = 0; i < m_eqs.size(); ++i) {
+        eq const& e = m_eqs[i];
+        vector<rational> len1, len2;
+        if (!is_complex(e)) {
+            continue;
+        }
+        if (e.ls().empty() || e.rs().empty() || 
+            (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) {
+            continue;
+        }
+
+        if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) {
+            change = true;
+            continue;
+        }
+        rational l1, l2;
+        for (unsigned j = 0; j < len1.size(); ++j) l1 += len1[j];
+        for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j];
+        if (l1 != l2) {
+            TRACE("seq", tout << "lengths are not compatible\n";);
+            expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr());
+            expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr());
+            expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m);
+            literal_vector lits;
+            propagate_eq(e.dep(), lits, lnl, lnr, false);
+            change = true;
+            continue;
+        }
+        if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) {
+            TRACE("seq", tout << "split lengths\n";);
+            return true;
+        }
+    }
+    return change;
+}
 
 
-    unsigned s = 0;
+bool theory_seq::is_complex(eq const& e) {
+    unsigned num_vars1 = 0, num_vars2 = 0;
+    for (unsigned i = 0; i < e.ls().size(); ++i) {
+        if (is_var(e.ls()[i])) ++num_vars1;
+    }
+    for (unsigned i = 0; i < e.rs().size(); ++i) {
+        if (is_var(e.rs()[i])) ++num_vars2;
+    }
+    return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2;
+}
+
+/*
+  \brief Decompose ls = rs into Xa = bYc, such that 
+   1. 
+    - X != Y
+    - |b| <= |X| <= |bY| in currrent model
+    - b is non-empty.
+   2. X != Y
+    - b is empty
+    - |X| <= |Y|
+   3. |X| = 0
+      - propagate X = empty      
+*/
+bool theory_seq::split_lengths(dependency* dep,
+                               expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                               vector<rational> const& ll, vector<rational> const& rl) {
+    context& ctx = get_context();
+    expr_ref X(m), Y(m), b(m);
+    if (ls.empty() || rs.empty()) {
+        return false;
+    } 
+    if (is_var(ls[0]) && ll[0].is_zero()) {
+        return set_empty(ls[0]);
+    }
+    if (is_var(rs[0]) && rl[0].is_zero()) {
+        return set_empty(rs[0]);
+    }
+    if (is_var(rs[0]) && !is_var(ls[0])) {
+        return split_lengths(dep, rs, ls, rl, ll);
+    }
+    if (!is_var(ls[0])) {
+        return false;
+    }
+    X = ls[0];
+    rational lenX = ll[0];
+    expr_ref_vector bs(m);
+    SASSERT(lenX.is_pos());
+    rational lenB(0), lenY(0);
+    for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) {
+        bs.push_back(rs[i]);
+        lenY = rl[i];
+        lenB += lenY;
+    }
+    SASSERT(lenX <= lenB);
+    SASSERT(!bs.empty());
+    Y = bs.back();
+    bs.pop_back();
+    if (!is_var(Y) && !m_util.str.is_unit(Y)) {
+        TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";);
+        return false;
+    }
+    if (X == Y) {
+        TRACE("seq", tout << "Cycle: " << X << "\n";);
+        return false;
+    }
+    if (lenY.is_zero()) {
+        return set_empty(Y);
+    }
+    b = mk_concat(bs, m.get_sort(X));
+
+    SASSERT(X != Y);
+
+
+    // |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2
+    expr_ref lenXE(m_util.str.mk_length(X), m);
+    expr_ref lenYE(m_util.str.mk_length(Y), m);
+    expr_ref lenb(m_util.str.mk_length(b), m);
+    expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m);
+    expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE), 
+                               m_autil.mk_int(0)), m);
+    literal  lit1(~mk_literal(le1));
+    literal  lit2(mk_literal(le2));
+    literal_vector lits;
+    lits.push_back(lit1);
+    lits.push_back(lit2);
+    
+    if (ctx.get_assignment(lit1) != l_true ||
+        ctx.get_assignment(lit2) != l_true) {
+        ctx.mark_as_relevant(lit1);
+        ctx.mark_as_relevant(lit2);
+    }
+    else if (m_util.str.is_unit(Y)) {
+        SASSERT(lenB == lenX);
+        bs.push_back(Y);
+        expr_ref bY(m_util.str.mk_concat(bs), m);
+        propagate_eq(dep, lits, X, bY, true);
+    }
+    else {
+        SASSERT(is_var(Y));
+        expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m);
+        expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m);
+        expr_ref bY1(m_util.str.mk_concat(b, Y1), m);
+        expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m);
+        propagate_eq(dep, lits, X, bY1, true);
+        propagate_eq(dep, lits, Y, Y1Y2, true);
+    }
+    return true;
+}
+
+bool theory_seq::set_empty(expr* x) {
+    add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x));
+    return true;
+}
+
+bool theory_seq::enforce_length(expr_ref_vector const& es, vector<rational> & len) {
+    bool all_have_length = true;
+    rational val;
+    zstring s;
+    for (unsigned i = 0; i < es.size(); ++i) {
+        expr* e = es[i];
+        if (m_util.str.is_unit(e)) {
+            len.push_back(rational(1));
+        } 
+        else if (m_util.str.is_empty(e)) {
+            len.push_back(rational(0));
+        }
+        else if (m_util.str.is_string(e, s)) {
+            len.push_back(rational(s.length()));
+        }
+        else if (get_length(e, val)) {
+            len.push_back(val);
+        }
+        else {
+            enforce_length(ensure_enode(e));
+            all_have_length = false;
+        }
+    }
+    return all_have_length;
+}
+
+bool theory_seq::branch_variable() {
+    context& ctx = get_context();
+    unsigned sz = m_eqs.size();
+    int start = ctx.get_random_value();
+
     for (unsigned i = 0; i < sz; ++i) {
         unsigned k = (i + start) % sz;
         eq const& e = m_eqs[k];
-        unsigned id = e.id();
 
-        s = find_branch_start(2*id);
-        TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
-        bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
-        insert_branch_start(2*id, s);
-        if (found) {
-            return true;
-        }
-        s = find_branch_start(2*id + 1);
-        found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
-        insert_branch_start(2*id + 1, s);
-        if (found) {
+        if (branch_variable(e)) {
             return true;
         }
 
@@ -338,6 +655,22 @@ bool theory_seq::branch_variable() {
     return ctx.inconsistent();
 }
 
+bool theory_seq::branch_variable(eq const& e) {
+    unsigned id = e.id();
+    unsigned s = find_branch_start(2*id);
+    TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";);
+    bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs());
+    insert_branch_start(2*id, s);
+    if (found) {
+        return true;
+    }
+    s = find_branch_start(2*id + 1);
+    found = find_branch_candidate(s, e.dep(), e.rs(), e.ls());
+    insert_branch_start(2*id + 1, s);
+    
+    return found;
+}
+
 void theory_seq::insert_branch_start(unsigned k, unsigned s) {
     m_branch_start.insert(k, s);
     m_trail_stack.push(pop_branch(k));
@@ -483,7 +816,6 @@ lbool theory_seq::assume_equality(expr* l, expr* r) {
         return l_false;
     }
     return ctx.get_assignment(mk_eq(l, r, false));
-    //return l_undef;
 }
 
 
@@ -1901,12 +2233,15 @@ void theory_seq::display(std::ostream & out) const {
 
 void theory_seq::display_equations(std::ostream& out) const {
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[i];
-        out << e.ls() << " = " << e.rs() << " <- \n";
-        display_deps(out, e.dep());
+        display_equation(out, m_eqs[i]);
     }
 }
 
+void theory_seq::display_equation(std::ostream& out, eq const& e) const {
+    out << e.ls() << " = " << e.rs() << " <- \n";
+    display_deps(out, e.dep());    
+}
+
 void theory_seq::display_disequations(std::ostream& out) const {
     bool first = true;
     for (unsigned i = 0; i < m_nqs.size(); ++i) {
@@ -3050,6 +3385,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     else if (m_util.str.is_in_re(e)) {
         propagate_in_re(e, is_true);
     }
+    else if (is_skolem(symbol("seq.split"), e)) {
+        // propagate equalities
+    }
     else {
         UNREACHABLE();
     }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 8206eeca4..fc37a8f06 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -358,6 +358,10 @@ namespace smt {
         void init_model(expr_ref_vector const& es);
         // final check 
         bool simplify_and_solve_eqs();   // solve unitary equalities
+        bool reduce_length_eq();
+        bool branch_unit_variable();     // branch on XYZ = abcdef
+        bool branch_binary_variable();   // branch on abcX = Ydefg 
+        bool branch_variable_mb();       // branch on a variable, model based on length
         bool branch_variable();          // branch on a variable
         bool split_variable();           // split a variable
         bool is_solved(); 
@@ -366,7 +370,16 @@ namespace smt {
         bool check_length_coherence(expr* e);
         bool fixed_length();
         bool fixed_length(expr* e);
+        void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units);
+        bool branch_variable(eq const& e);
+        bool branch_binary_variable(eq const& e);
+        bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool propagate_length_coherence(expr* e);  
+        bool split_lengths(dependency* dep,
+                           expr_ref_vector const& ls, expr_ref_vector const& rs, 
+                           vector<rational> const& ll, vector<rational> const& rl);
+        bool set_empty(expr* x);
+        bool is_complex(eq const& e);
 
         bool check_extensionality();
         bool check_contains();
@@ -465,6 +478,7 @@ namespace smt {
         bool has_length(expr *e) const { return m_length.contains(e); }
         void add_length(expr* e);
         void enforce_length(enode* n);
+        bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
         void enforce_length_coherence(enode* n1, enode* n2);
 
         void add_elim_string_axiom(expr* n);
@@ -532,6 +546,7 @@ namespace smt {
 
         // diagnostics
         void display_equations(std::ostream& out) const;
+        void display_equation(std::ostream& out, eq const& e) const;
         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;