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/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h
index 5c572907e..327763da4 100644
--- a/src/ackermannization/ackr_helper.h
+++ b/src/ackermannization/ackr_helper.h
@@ -33,19 +33,12 @@ class ackr_helper {
          which are not marked as uninterpreted but effectively are.
         */
         inline bool should_ackermannize(app const * a) const {
-            if (a->get_family_id() == m_bvutil.get_family_id()) {
-                switch (a->get_decl_kind()) {
-                    case OP_BSDIV0:
-                    case OP_BUDIV0:
-                    case OP_BSREM0:
-                    case OP_BUREM0:
-                    case OP_BSMOD0:
-                        return true;
-                    default:
-                        return is_uninterp(a);
-                }
+            if (is_uninterp(a))
+                return true;
+            else {
+                decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
+                return p->is_considered_uninterpreted(a->get_decl());
             }
-            return (is_uninterp(a));
         }
 
         inline bv_util& bvutil() { return m_bvutil; }
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..414854f3a
--- /dev/null
+++ b/src/ast/rewriter/bv_trailing.cpp
@@ -0,0 +1,401 @@
+/*++
+ 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;
+
+    // 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(mk_extract.m()) {
+            for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
+                m_count_cache[i] = NULL;
+    }
+
+    virtual ~imp() {
+        reset_cache(0);
+    }
+
+    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 && !new_last) {// all args eaten completely
+            SASSERT(retv == m_util.get_bv_size(a));
+            result = NULL;
+            return retv;
+        }
+
+        expr_ref_vector new_args(m);
+        for (unsigned j = 0; j < i; ++j)
+            new_args.push_back(a->get_arg(j));
+        if (new_last) 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(std::min(n, sz), 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() {
+    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/model/func_interp.cpp b/src/model/func_interp.cpp
index 90810f294..5c53e64ba 100644
--- a/src/model/func_interp.cpp
+++ b/src/model/func_interp.cpp
@@ -104,9 +104,55 @@ void func_interp::reset_interp_cache() {
     m_manager.dec_ref(m_interp);
     m_interp = 0;
 }
-    
+
+bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
+    args.reset();
+    if (!is_app(e) || !m().is_ite(to_app(e)))
+        return false;
+
+    app * a = to_app(e);
+    expr * c = a->get_arg(0);
+    expr * t = a->get_arg(1);
+    expr * f = a->get_arg(2);
+
+    if ((m_arity == 0) ||
+        (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||
+        (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
+        return false;
+
+    args.resize(m_arity, 0);
+    for (unsigned i = 0; i < m_arity; i++) {
+        expr * ci = (m_arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i);
+
+        if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2)
+            return false;
+
+        expr * a0 = to_app(ci)->get_arg(0);
+        expr * a1 = to_app(ci)->get_arg(1);
+        if (is_var(a0) && to_var(a0)->get_idx() == i)
+            args[i] = a1;
+        else if (is_var(a1) && to_var(a1)->get_idx() == i)
+            args[i] = a0;
+        else
+            return false;
+    }
+
+    return true;
+}
+
 void func_interp::set_else(expr * e) {
+    if (e == m_else)
+        return;
+
     reset_interp_cache();
+
+    ptr_vector<expr> args;
+    while (e && is_fi_entry_expr(e, args)) {
+        TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;);
+        insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
+        e = to_app(e)->get_arg(2);
+    }
+
     m_manager.inc_ref(e);
     m_manager.dec_ref(m_else);
     m_else = e;
@@ -148,7 +194,7 @@ func_entry * func_interp::get_entry(expr * const * args) const {
 
 void func_interp::insert_entry(expr * const * args, expr * r) {
     reset_interp_cache();
-    func_entry * entry = get_entry(args); 
+    func_entry * entry = get_entry(args);
     if (entry != 0) {
         entry->set_result(m_manager, r);
         return;
@@ -201,7 +247,7 @@ expr * func_interp::get_max_occ_result() const {
     for (; it != end; ++it) {
         func_entry * curr = *it;
         expr * r = curr->get_result();
-        unsigned occs = 0; 
+        unsigned occs = 0;
         num_occs.find(r, occs);
         occs++;
         num_occs.insert(r, occs);
@@ -283,13 +329,13 @@ expr * func_interp::get_interp() const {
     return r;
 }
 
-func_interp * func_interp::translate(ast_translation & translator) const {    
+func_interp * func_interp::translate(ast_translation & translator) const {
     func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
 
     ptr_vector<func_entry>::const_iterator it  = m_entries.begin();
     ptr_vector<func_entry>::const_iterator end = m_entries.end();
     for (; it != end; ++it) {
-        func_entry * curr = *it;        
+        func_entry * curr = *it;
         ptr_buffer<expr> new_args;
         for (unsigned i=0; i<m_arity; i++)
             new_args.push_back(translator(curr->get_arg(i)));
diff --git a/src/model/func_interp.h b/src/model/func_interp.h
index b264f4f1d..d0d61546e 100644
--- a/src/model/func_interp.h
+++ b/src/model/func_interp.h
@@ -12,7 +12,7 @@ Abstract:
     modulo a model.
 
     Main goal: Remove some code duplication and make the evaluator more efficient.
-    
+
     Example of code duplication that existed in Z3:
       - smt_model_generator was creating func_values that were essentially partial func_interps
       - smt_model_generator was creating if-then-else (lambda) exprs representing func_values
@@ -39,17 +39,17 @@ class func_entry {
     bool   m_args_are_values; //!< true if is_value(m_args[i]) is true for all i in [0, arity)
 
     // m_result and m_args[i] must be ground terms.
-    
+
     expr * m_result;
     expr * m_args[];
 
     static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); }
     func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result);
-    
+
     friend class func_interp;
-    
+
     void set_result(ast_manager & m, expr * r);
-    
+
 public:
     static func_entry * mk(ast_manager & m, unsigned arity, expr * const * args, expr * result);
     bool args_are_values() const { return m_args_are_values; }
@@ -69,7 +69,7 @@ class func_interp {
     ptr_vector<func_entry> m_entries;
     expr *                 m_else;
     bool                   m_args_are_values; //!< true if forall e in m_entries e.args_are_values() == true
-    
+
     expr *                 m_interp; //!< cache for representing the whole interpretation as a single expression (it uses ite terms).
 
     void reset_interp_cache();
@@ -83,7 +83,7 @@ public:
     ast_manager & m () const { return m_manager; }
 
     func_interp * copy() const;
-    
+
     unsigned get_arity() const { return m_arity; }
 
     bool is_partial() const { return m_else == 0; }
@@ -95,7 +95,7 @@ public:
 
     expr * get_else() const { return m_else; }
     void set_else(expr * e);
-    
+
     void insert_entry(expr * const * args, expr * r);
     void insert_new_entry(expr * const * args, expr * r);
     func_entry * get_entry(expr * const * args) const;
@@ -110,6 +110,9 @@ public:
     expr * get_interp() const;
 
     func_interp * translate(ast_translation & translator) const;
+
+private:
+    bool is_fi_entry_expr(expr * e, ptr_vector<expr> & args);
 };
 
 #endif
diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp
index 54c654d54..d4e738ed7 100644
--- a/src/tactic/bv/bvarray2uf_rewriter.cpp
+++ b/src/tactic/bv/bvarray2uf_rewriter.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"ast_pp.h"
 #include"bvarray2uf_rewriter.h"
 #include"rewriter_def.h"
+#include"ref_util.h"
 
 // [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
 //     Quantified Bit-Vector Formulas, in Formal Methods in System Design,
@@ -50,10 +51,7 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con
 }
 
 bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
-    for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
-    it != m_arrays_fs.end();
-        it++)
-        m_manager.dec_ref(it->m_value);
+    dec_ref_map_key_values(m_manager, m_arrays_fs);
 }
 
 void bvarray2uf_rewriter_cfg::reset() {}
@@ -110,12 +108,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
     if (m_array_util.is_as_array(e))
         return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
     else {
-        app * a = to_app(e);
         func_decl * bv_f = 0;
         if (!m_arrays_fs.find(e, bv_f)) {
-            sort * domain = get_index_sort(a);
-            sort * range = get_value_sort(a);
+            sort * domain = get_index_sort(e);
+            sort * range = get_value_sort(e);
             bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
+            TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " new func_decl is " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(to_app(e)->get_decl(),
@@ -124,8 +122,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
             else if (m_fmc)
                 m_fmc->insert(bv_f);
             m_arrays_fs.insert(e, bv_f);
+            m_manager.inc_ref(e);
             m_manager.inc_ref(bv_f);
         }
+        else {
+            TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " found " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
+        }
 
         return func_decl_ref(bv_f, m_manager);
     }
@@ -138,18 +140,24 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         SASSERT(num == 2);
         // From [1]: Finally, we replace equations of the form t = s,
         // where t and s are arrays, with \forall x . f_t(x) = f_s(x).
-        func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
-        func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
+        if (m_manager.are_equal(args[0], args[1])) {
+            result = m_manager.mk_true();
+            res = BR_DONE;
+        }
+        else {
+            func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
+            func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
 
-        sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
-        symbol names[1] = { symbol("x") };
-        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+            sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
+            symbol names[1] = { symbol("x") };
+            var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
 
-        expr_ref body(m_manager);
-        body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
+            expr_ref body(m_manager);
+            body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
 
-        result = m_manager.mk_forall(1, sorts, names, body);
-        res = BR_DONE;
+            result = m_manager.mk_forall(1, sorts, names, body);
+            res = BR_DONE;
+        }
     }
     else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
         result = m_manager.mk_distinct_expanded(num, args);
@@ -310,7 +318,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         }
     }
 
-    CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
+    CTRACE("bvarray2uf_rw", res == BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
     return res;
 }
 
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index 42ceaf78c..ecf1889a2 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -62,7 +62,6 @@ class bvarray2uf_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             tactic_report report("bvarray2uf", *g);
             mc = 0; pc = 0; core = 0; result.reset();
-            fail_if_proof_generation("bvarray2uf", g);
             fail_if_unsat_core_generation("bvarray2uf", g);
 
             TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
@@ -73,7 +72,6 @@ class bvarray2uf_tactic : public tactic {
                 filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
                 mc = concat(emc, fmc);
                 m_rw.set_mcs(emc, fmc);
-
             }
 
 
@@ -86,10 +84,10 @@ class bvarray2uf_tactic : public tactic {
                     break;
                 expr * curr = g->form(idx);
                 m_rw(curr, new_curr, new_pr);
-                //if (m_produce_proofs) {
-                //    proof * pr = g->pr(idx);
-                //    new_pr = m.mk_modus_ponens(pr, new_pr);
-                //}
+                if (m_produce_proofs) {
+                    proof * pr = g->pr(idx);
+                    new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+                }
                 g->update(idx, new_curr, new_pr, g->dep(idx));
             }
 
@@ -143,7 +141,7 @@ public:
     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/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp
index ebd530a58..cdd096455 100644
--- a/src/tactic/extension_model_converter.cpp
+++ b/src/tactic/extension_model_converter.cpp
@@ -43,41 +43,6 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
     }
 }
 
-bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args) {
-    args.reset();
-    if (!is_app(e) || !m().is_ite(to_app(e)))
-        return false;
-
-    app * a = to_app(e);
-    expr * c = a->get_arg(0);
-    expr * t = a->get_arg(1);
-    expr * f = a->get_arg(2);
-
-    if ((arity == 0) ||
-        (arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||
-        (arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity)))
-        return false;
-
-    args.resize(arity, 0);
-    for (unsigned i = 0; i < arity; i++) {
-        expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i);
-
-        if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2)
-            return false;
-
-        expr * a0 = to_app(ci)->get_arg(0);
-        expr * a1 = to_app(ci)->get_arg(1);
-        if (is_var(a0) && to_var(a0)->get_idx() == i)
-            args[i] = a1;
-        else if (is_var(a1) && to_var(a1)->get_idx() == i)
-            args[i] = a0;
-        else
-            return false;
-    }
-
-    return true;
-}
-
 void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
     SASSERT(goal_idx == 0);
     TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
@@ -97,14 +62,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
         }
         else {
             func_interp * new_fi = alloc(func_interp, m(), arity);
-            expr * e = val.get();
-            ptr_vector<expr> args;
-            while (is_fi_entry_expr(e, arity, args)) {
-                TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;);
-                new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
-                e = to_app(e)->get_arg(2);
-            }
-            new_fi->set_else(e);
+            new_fi->set_else(val);
             md->register_decl(f, new_fi);
         }
     }
diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h
index 9431906f3..46644eec2 100644
--- a/src/tactic/extension_model_converter.h
+++ b/src/tactic/extension_model_converter.h
@@ -43,9 +43,6 @@ public:
     void insert(func_decl * v, expr * def);
 
     virtual model_converter * translate(ast_translation & translator);
-
-private:
-    bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args);
 };