diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 0c77867d4..93d0edf2f 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -447,6 +447,8 @@ public:
     app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(arith_family_id, OP_ADD, arg1, arg2, arg3); }
     app * mk_add(expr_ref_vector const& args) const { return mk_add(args.size(), args.data()); }
     app * mk_add(expr_ref_buffer const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_buffer<expr> const& args) const { return mk_add(args.size(), args.data()); }
+    app * mk_add(ptr_vector<expr> const& args) const { return mk_add(args.size(), args.data()); }
 
     app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(arith_family_id, OP_SUB, arg1, arg2); }
     app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(arith_family_id, OP_SUB, num_args, args); }
diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h
index 83d541097..79c6e682e 100644
--- a/src/ast/array_decl_plugin.h
+++ b/src/ast/array_decl_plugin.h
@@ -207,6 +207,10 @@ public:
         return mk_store(args.size(), args.data());
     }
 
+    app* mk_store(ptr_buffer<expr> const& args) const {
+        return mk_store(args.size(), args.data());
+    }
+
     app * mk_select(unsigned num_args, expr * const * args) const {
         return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
     }
diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h
index 37531d936..ee618b42c 100644
--- a/src/ast/bv_decl_plugin.h
+++ b/src/ast/bv_decl_plugin.h
@@ -448,9 +448,17 @@ public:
     app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
     app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); }
     app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); }
+    app * mk_bv_add(ptr_buffer<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(ptr_vector<expr> const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_vector const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
+    app * mk_bv_add(expr_ref_buffer const & args) const { return m_manager.mk_app(get_fid(), OP_BADD, args.size(), args.data()); }
     app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); }
     app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); }
     app * mk_bv_mul(unsigned n, expr* const* args) const { return m_manager.mk_app(get_fid(), OP_BMUL, n, args); }
+    app* mk_bv_mul(ptr_buffer<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(ptr_vector<expr> const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_vector const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
+    app* mk_bv_mul(expr_ref_buffer const& args) const { return m_manager.mk_app(get_fid(), OP_BMUL, args.size(), args.data()); }
     app * mk_bv_udiv(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV, arg1, arg2); }
     app * mk_bv_udiv_i(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUDIV_I, arg1, arg2); }
     app * mk_bv_udiv0(expr * arg) const { return m_manager.mk_app(get_fid(), OP_BUDIV0, arg); }
diff --git a/src/ast/converters/CMakeLists.txt b/src/ast/converters/CMakeLists.txt
index 52895f064..64f5060e7 100644
--- a/src/ast/converters/CMakeLists.txt
+++ b/src/ast/converters/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(converters
   SOURCES
+    expr_inverter.cpp
     equiv_proof_converter.cpp
     generic_model_converter.cpp
     horn_subsume_model_converter.cpp
diff --git a/src/ast/converters/expr_inverter.cpp b/src/ast/converters/expr_inverter.cpp
new file mode 100644
index 000000000..504c04ab0
--- /dev/null
+++ b/src/ast/converters/expr_inverter.cpp
@@ -0,0 +1,791 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    expr_inverter.cpp
+
+Abstract:
+
+    inverter interface and instance
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-11
+
+--*/
+
+#include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_util.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/converters/expr_inverter.h"
+
+class basic_expr_inverter : public iexpr_inverter {
+public:
+
+    basic_expr_inverter(ast_manager& m) : iexpr_inverter(m) {}
+
+    /**
+     * if (c, x, x') -> fresh
+     * x := fresh
+     * x' := fresh
+     * 
+     * if (x, x', e) -> fresh
+     * x := true
+     * x' := fresh
+     * 
+     * if (x, t, x') -> fresh
+     * x := false
+     * x' := fresh
+     * 
+     * not x -> fresh
+     * x := not fresh
+     * 
+     * x & x' -> fresh
+     * x := fresh
+     * x' := true
+     * 
+     * x or x' -> fresh
+     * x := fresh
+     * x' := false
+     *
+     * x = t -> fresh
+     * x := if(fresh, t, diff(t))
+     * where diff is a diagnonalization function available in domains of size > 1.
+     *
+     */
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) {
+        SASSERT(f->get_family_id() == m.get_basic_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_ITE:
+            SASSERT(num == 3);
+            if (uncnstr(args[1]) && uncnstr(args[2])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[1], r);
+                add_def(args[2], r);
+                return true;
+            }
+            if (uncnstr(args[0]) && uncnstr(args[1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_true());
+                add_def(args[1], r);
+                return true;
+            }
+            if (uncnstr(args[0]) && uncnstr(args[2])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_false());
+                add_def(args[2], r);
+                return true;
+            }
+            return false;
+        case OP_NOT:
+            SASSERT(num == 1);
+            if (uncnstr(args[0])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_def(args[0], m.mk_not(r));
+                return true;
+            }
+            return false;
+        case OP_AND:
+            if (num > 0 && uncnstr(num, args)) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_defs(num, args, r, m.mk_true());
+                return true;
+            }
+            return false;
+        case OP_OR:
+            if (num > 0 && uncnstr(num, args)) {
+                mk_fresh_uncnstr_var_for(f, r);
+                add_defs(num, args, r, m.mk_false());
+                return true;
+            }
+            return false;
+        case OP_EQ:
+            SASSERT(num == 2);
+            // return process_eq(f, args[0], args[1]);
+        default:
+            return false;
+        }        
+        return false;
+    }
+    
+    bool mk_diff(expr* t, expr_ref& r) override {
+        SASSERT(m.is_bool(t));
+        r = mk_not(m, t);
+        return true;
+    }
+};
+
+class arith_expr_inverter : public iexpr_inverter {
+    arith_util a;
+public:
+
+    arith_expr_inverter(ast_manager& m) : iexpr_inverter(m), a(m) {}
+
+    family_id get_fid() const { return a.get_family_id(); }
+
+    bool process_le_ge(func_decl* f, expr* arg1, expr* arg2, bool le, expr_ref& r) {
+        expr* v;
+        expr* t;
+        if (uncnstr(arg1)) {
+            v = arg1;
+            t = arg2;
+        }
+        else if (uncnstr(arg2)) {
+            v = arg2;
+            t = arg1;
+            le = !le;
+        }
+        else 
+            return false;
+        
+        mk_fresh_uncnstr_var_for(f, r);
+        if (m_mc) {
+            // v = ite(u, t, t + 1) if le
+            // v = ite(u, t, t - 1) if !le
+            add_def(v, m.mk_ite(r, t, a.mk_add(t, a.mk_numeral(rational(le ? 1 : -1), arg1->get_sort()))));
+        }
+        return true;
+    }
+
+    bool process_add(unsigned num, expr* const* args, expr_ref& u) {
+        if (num == 0)
+            return false;
+        unsigned i;
+        expr* v = nullptr;
+        for (i = 0; i < num; i++) {
+            expr* arg = args[i];
+            if (uncnstr(arg)) {
+                v = arg;
+                break;
+            }
+        }
+        if (v == nullptr)
+            return false;
+        mk_fresh_uncnstr_var_for(v->get_sort(), u);
+        if (!m_mc)
+            return true;
+        ptr_buffer<expr> new_args;
+        for (unsigned j = 0; j < num; j++) 
+            if (j != i)
+                new_args.push_back(args[j]);
+        
+        if (new_args.empty()) 
+            add_def(v, u);
+        else {
+            expr* rest = a.mk_add(new_args); 
+            add_def(v, a.mk_sub(u, rest));
+        }
+        return true;
+    }
+
+    bool process_arith_mul(unsigned num, expr* const* args, expr_ref & u) {
+        if (num == 0)
+            return false;
+        sort* s = args[0]->get_sort();
+        if (uncnstr(num, args)) {
+            mk_fresh_uncnstr_var_for(s, u);
+            if (m_mc)
+                add_defs(num, args, u, a.mk_numeral(rational(1), s));
+            return true;
+        }
+        // c * v case for reals
+        bool is_int;
+        rational val;
+        if (num == 2 && uncnstr(args[1]) && a.is_numeral(args[0], val, is_int) && !is_int) {
+            if (val.is_zero())
+                return false;
+            mk_fresh_uncnstr_var_for(s, u);
+            if (m_mc) {
+                val = rational(1) / val;
+                add_def(args[1], a.mk_mul(a.mk_numeral(val, false), u));
+            }
+            return true;
+        }
+        return false;
+    }
+
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override {
+        SASSERT(f->get_family_id() == a.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_ADD:
+            return process_add(num, args, r);
+        case OP_MUL:
+            return process_arith_mul(num, args, r);
+        case OP_LE:
+            SASSERT(num == 2);
+            return process_le_ge(f, args[0], args[1], true, r);
+        case OP_GE:
+            SASSERT(num == 2);
+            return process_le_ge(f, args[0], args[1], false, r);
+        default:
+            return false;
+        }
+    }
+
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        SASSERT(a.is_int_real(t));
+        r = a.mk_add(t, a.mk_numeral(rational(1), a.is_int(t)));
+        return true;
+    }
+};
+
+class bv_expr_inverter : public iexpr_inverter {
+    bv_util bv;
+
+    bool process_add(unsigned num, expr* const* args, expr_ref& u) {
+        if (num == 0)
+            return false;
+        unsigned i;
+        expr* v = nullptr;
+        for (i = 0; i < num; i++) {
+            expr* arg = args[i];
+            if (uncnstr(arg)) {
+                v = arg;
+                break;
+            }
+        }
+        if (!v)
+            return false;
+        mk_fresh_uncnstr_var_for(v->get_sort(), u);
+        if (!m_mc)
+            return true;
+        ptr_buffer<expr> new_args;
+        for (unsigned j = 0; j < num; j++)
+            if (j != i)
+                new_args.push_back(args[j]);
+
+        if (new_args.empty())
+            add_def(v, u);
+        else {
+            expr* rest = bv.mk_bv_add(new_args);
+            add_def(v, bv.mk_bv_sub(u, rest));
+        }
+        return true;
+    }
+
+    bool process_bv_mul(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+        if (num == 0)
+            return nullptr;
+        if (uncnstr(num, args)) {
+            sort* s = args[0]->get_sort();
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc)
+                add_defs(num, args, r, bv.mk_numeral(rational(1), s));
+            return true;
+        }
+        // c * v (c is odd) case
+        unsigned sz;
+        rational val;
+        rational inv;
+        if (num == 2 &&
+            uncnstr(args[1]) &&
+            bv.is_numeral(args[0], val, sz) &&
+            val.mult_inverse(sz, inv)) {
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc)
+                add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv, sz), r));
+            return true;
+        }
+
+        //
+        // x * K -> fresh[hi-sh-1:0] ++ 0...0
+        // where sh = parity of K
+        // then x -> J^-1*fresh 
+        // where J = K >> sh
+        // Because x * K = fresh * K * J^-1 = fresh * 2^sh = fresh[hi-sh-1:0] ++ 0...0
+        //
+        if (num == 2 &&
+            uncnstr(args[1]) &&
+            bv.is_numeral(args[0], val, sz) &&
+            val.is_pos()) {
+            unsigned sh = 0;
+            while (val.is_even()) {
+                val /= rational(2);
+                ++sh;
+            }
+            mk_fresh_uncnstr_var_for(f, r);
+            if (sh > 0)
+                r = bv.mk_concat(bv.mk_extract(sz - sh - 1, 0, r), bv.mk_numeral(0, sh));
+
+            if (m_mc) {
+                rational inv_r;
+                VERIFY(val.mult_inverse(sz, inv_r));
+                add_def(args[1], bv.mk_bv_mul(bv.mk_numeral(inv_r, sz), r)); 
+            }
+            return true;
+        }
+
+        //
+        // assume x is unconstrained, we can handle general multiplication as follows: 
+        // x * y -> if y = 0 then y else fresh << parity(y)
+        // and x -> if y = 0 then y else (y >> parity(y))^-1
+        // parity can be defined using a "giant" ite expression.
+        //
+
+        return false;
+    }
+
+
+    bool process_extract(func_decl* f, expr* arg, expr_ref& r) {
+        if (!uncnstr(arg))
+            return false;
+        mk_fresh_uncnstr_var_for(f, r);
+        if (!m_mc)
+            return true;
+        unsigned high = bv.get_extract_high(f);
+        unsigned low = bv.get_extract_low(f);
+        unsigned bv_size = bv.get_bv_size(arg->get_sort());
+        if (bv_size == high - low + 1) 
+            add_def(arg, r);        
+        else {
+            ptr_buffer<expr> args;
+            if (high < bv_size - 1)
+                args.push_back(bv.mk_numeral(rational(0), bv_size - high - 1));
+            args.push_back(r);
+            if (low > 0)
+                args.push_back(bv.mk_numeral(rational(0), low));
+            add_def(arg, bv.mk_concat(args.size(), args.data()));
+        }
+        return true;
+    }
+
+    bool process_bv_div(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
+        if (uncnstr(arg1) && uncnstr(arg2)) {
+            sort* s = arg1->get_sort();
+            mk_fresh_uncnstr_var_for(f, r);
+            if (m_mc) {
+                add_def(arg1, r);
+                add_def(arg2, bv.mk_numeral(rational(1), s));
+            }
+            return true;
+        }
+        return false;
+    }
+
+    bool process_concat(func_decl* f, unsigned num, expr* const* args, expr_ref& r) {
+        if (num == 0)
+            return false;
+        if (!uncnstr(num, args))
+            return false;
+        mk_fresh_uncnstr_var_for(f, r);
+        if (m_mc) {
+            unsigned i = num;
+            unsigned low = 0;
+            while (i > 0) {
+                --i;
+                expr* arg = args[i];
+                unsigned sz = bv.get_bv_size(arg);
+                add_def(arg, bv.mk_extract(low + sz - 1, low, r));
+                low += sz;
+            }
+        }
+        return true;
+    }
+
+    bool process_bv_le(func_decl* f, expr* arg1, expr* arg2, bool is_signed, expr_ref& r) {
+        if (uncnstr(arg1)) {
+            // v <= t
+            expr* v = arg1;
+            expr* t = arg2;
+            // v <= t --->  (u or t == MAX)   u is fresh
+            //     add definition v = ite(u or t == MAX, t, t+1)
+            unsigned bv_sz = bv.get_bv_size(arg1);
+            rational MAX;
+            if (is_signed)
+                MAX = rational::power_of_two(bv_sz - 1) - rational(1);
+            else
+                MAX = rational::power_of_two(bv_sz) - rational(1);
+            mk_fresh_uncnstr_var_for(f, r);
+            r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MAX, bv_sz)));
+            if (m_mc)
+                add_def(v, m.mk_ite(r, t, bv.mk_bv_add(t, bv.mk_numeral(rational(1), bv_sz))));
+            return true;
+        }
+        if (uncnstr(arg2)) {
+            // v >= t
+            expr* v = arg2;
+            expr* t = arg1;
+            // v >= t --->  (u ot t == MIN)  u is fresh
+            //    add definition v = ite(u or t == MIN, t, t-1)
+            unsigned bv_sz = bv.get_bv_size(arg1);
+            rational MIN;
+            if (is_signed)
+                MIN = -rational::power_of_two(bv_sz - 1);
+            else
+                MIN = rational(0);
+            mk_fresh_uncnstr_var_for(f, r);
+            r = m.mk_or(r, m.mk_eq(t, bv.mk_numeral(MIN, bv_sz)));
+            if (m_mc)
+                add_def(v, m.mk_ite(r, t, bv.mk_bv_sub(t, bv.mk_numeral(rational(1), bv_sz))));
+            return true;
+        }
+        return false;
+    }
+
+    bool process_bvnot(expr* e, expr_ref& r) {
+        if (!uncnstr(e))
+            return false;
+        mk_fresh_uncnstr_var_for(e->get_sort(), r);
+        if (m_mc)
+            add_def(e, bv.mk_bv_not(r));
+        return true;
+    }
+
+    public:
+        bv_expr_inverter(ast_manager& m) : iexpr_inverter(m), bv(m) {}
+
+        family_id get_fid() const { return bv.get_family_id(); }
+
+    /**
+     * x + t -> fresh
+     * x := fresh - t
+     *
+     * x * x' * x'' -> fresh
+     * x := fresh
+     * x', x'' := 1
+     *
+     * c * x -> fresh, c is odd
+     * x := fresh*c^-1
+     *
+     * x[sz-1:0] -> fresh
+     * x := fresh
+     *
+     * x[hi:lo] -> fresh
+     * x := fresh1 ++ fresh ++ fresh2
+     *
+     * x udiv x', x sdiv x' -> fresh
+     * x' := 1
+     * x := fresh
+     *
+     * x ++ x' ++ x'' -> fresh
+     * x   := fresh[hi1:lo1]
+     * x'  := fresh[hi2:lo2]
+     * x'' := fresh[hi3:lo3]
+     *
+     * x <= t -> fresh or t == MAX
+     * x := if(fresh, t, t + 1)
+     * t <= x -> fresh or t == MIN
+     * x := if(fresh, t, t - 1)
+     *
+     * ~x -> fresh
+     * x := ~fresh
+     *
+     * x | y -> fresh
+     * x := fresh
+     * y := 0
+     *
+     */
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override {
+        SASSERT(f->get_family_id() == bv.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_BADD:
+            return process_add(num, args, r);
+        case OP_BMUL:
+            return process_bv_mul(f, num, args, r);
+        case OP_BSDIV:
+        case OP_BUDIV:
+        case OP_BSDIV_I:
+        case OP_BUDIV_I:
+            SASSERT(num == 2);
+            return process_bv_div(f, args[0], args[1], r);
+        case OP_SLEQ:
+            SASSERT(num == 2);
+            return process_bv_le(f, args[0], args[1], true, r);
+        case OP_ULEQ:
+            SASSERT(num == 2);
+            return process_bv_le(f, args[0], args[1], false, r);
+        case OP_CONCAT:
+            return process_concat(f, num, args, r);
+        case OP_EXTRACT:
+            SASSERT(num == 1);
+            return process_extract(f, args[0], r);
+        case OP_BNOT:
+            SASSERT(num == 1);
+            return process_bvnot(args[0], r);
+        case OP_BOR:
+            if (num > 0 && uncnstr(num, args)) {
+                sort* s = args[0]->get_sort();
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc)
+                    add_defs(num, args, r, bv.mk_numeral(rational(0), s));
+                return true;
+            }
+            return false;
+        default:
+            return false;
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        r = bv.mk_bv_not(t);
+        return true;
+    }
+};
+
+
+
+/**
+ * F[select(x, i)] -> F[fresh]
+ * x := const(fresh)
+
+ * F[store(x, ..., x')] -> F[fresh]
+ * x' := select(x, ...)
+ * x := fresh
+ */
+
+class array_expr_inverter : public iexpr_inverter {
+    array_util a;
+    iexpr_inverter& inv;
+public:
+    array_expr_inverter(ast_manager& m, iexpr_inverter& s) : iexpr_inverter(m), a(m), inv(s) {}
+
+    family_id get_fid() const { return a.get_family_id(); }
+
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override {
+        SASSERT(f->get_family_id() == a.get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_SELECT:
+            if (uncnstr(args[0])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                sort* s = args[0]->get_sort();
+                if (m_mc)
+                    add_def(args[0], a.mk_const_array(s, r));
+                return true;
+            }
+            return false;
+        case OP_STORE:
+            if (uncnstr(args[0]) && uncnstr(args[num - 1])) {
+                mk_fresh_uncnstr_var_for(f, r);
+                if (m_mc) {
+                    add_def(args[num - 1], m.mk_app(a.get_family_id(), OP_SELECT, num - 1, args));
+                    add_def(args[0], r);
+                }
+                return true;
+            }
+        default:
+            return false;
+        }
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        sort* s = t->get_sort();
+        SASSERT(a.is_array(s));
+        if (m.is_uninterp(get_array_range(s)))
+            return false;
+        unsigned arity = get_array_arity(s);
+        for (unsigned i = 0; i < arity; i++)
+            if (m.is_uninterp(get_array_domain(s, i)))
+                return false;
+        // building 
+        // r = (store t i1 ... in d)
+        // where i1 ... in are arbitrary values
+        // and d is a term different from (select t i1 ... in)
+        expr_ref_vector new_args(m);
+        new_args.push_back(t);
+        for (unsigned i = 0; i < arity; i++)
+            new_args.push_back(m.get_some_value(get_array_domain(s, i)));
+        expr_ref sel(m);
+        sel = a.mk_select(new_args);
+        expr_ref diff_sel(m);
+        if (!inv.mk_diff(sel, diff_sel))
+            return false;
+        new_args.push_back(diff_sel);
+        r = a.mk_store(new_args);
+        return true;
+    }
+};
+
+
+
+class dt_expr_inverter : public iexpr_inverter {
+    datatype_util dt;
+public:
+
+    dt_expr_inverter(ast_manager& m) : iexpr_inverter(m), dt(m) {}
+
+    family_id get_fid() const { return dt.get_family_id(); }
+    /**
+     *   head(x) -> fresh
+     *   x := cons(fresh, arb)
+     */
+    bool operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& r, expr_ref& side_cond) override {
+        if (dt.is_accessor(f)) {
+            SASSERT(num == 1);
+            if (uncnstr(args[0])) {
+                if (!m_mc) {
+                    mk_fresh_uncnstr_var_for(f, r);
+                    return true;
+                }
+                func_decl* c = dt.get_accessor_constructor(f);
+                for (unsigned i = 0; i < c->get_arity(); i++)
+                    if (!m.is_fully_interp(c->get_domain(i)))
+                        return false;
+                mk_fresh_uncnstr_var_for(f, r);
+                ptr_vector<func_decl> const& accs = *dt.get_constructor_accessors(c);
+                ptr_buffer<expr> new_args;
+                for (unsigned i = 0; i < accs.size(); i++) {
+                    if (accs[i] == f)
+                        new_args.push_back(r);
+                    else
+                        new_args.push_back(m.get_some_value(c->get_domain(i)));
+                }
+                add_def(args[0], m.mk_app(c, new_args));
+                return true;
+            }
+        }
+        return false;
+    }
+
+    bool mk_diff(expr* t, expr_ref& r) override {
+        // In the current implementation, I only handle the case where
+        // the datatype has a recursive constructor.
+        sort* s = t->get_sort();
+        ptr_vector<func_decl> const& constructors = *dt.get_datatype_constructors(s);
+        for (func_decl* constructor : constructors) {
+            unsigned num = constructor->get_arity();
+            unsigned target = UINT_MAX;
+            for (unsigned i = 0; i < num; i++) {
+                sort* s_arg = constructor->get_domain(i);
+                if (s == s_arg) {
+                    target = i;
+                    continue;
+                }
+                if (m.is_uninterp(s_arg))
+                    break;
+            }
+            if (target == UINT_MAX)
+                continue;
+            // use the constructor the distinct term constructor(...,t,...)
+            ptr_buffer<expr> new_args;
+            for (unsigned i = 0; i < num; i++) {
+                if (i == target) 
+                    new_args.push_back(t);
+                else 
+                    new_args.push_back(m.get_some_value(constructor->get_domain(i)));
+            }
+            r = m.mk_app(constructor, new_args);
+            return true;
+        }
+        return false;
+    }
+};
+
+
+
+expr_inverter::~expr_inverter() {
+    for (auto* v : m_inverters)
+        dealloc(v);
+}
+
+
+bool iexpr_inverter::uncnstr(unsigned num, expr * const * args) const {
+    for (unsigned i = 0; i < num; i++)
+        if (!m_is_var(args[i]))
+            return false;
+    return true;
+}
+
+/**
+   \brief Create a fresh variable for abstracting (f args[0] ... args[num-1])
+   Return true if it a new variable was created, and false if the variable already existed for this
+   application. Store the variable in v
+*/
+void iexpr_inverter::mk_fresh_uncnstr_var_for(sort * s, expr_ref & v) {
+    v = m.mk_fresh_const(nullptr, s);
+    if (m_mc) 
+        m_mc->hide(v);
+}
+
+void iexpr_inverter::add_def(expr * v, expr * def) {
+    expr_ref _v(v, m);
+    expr_ref _d(def, m);
+    if (!m_mc)
+        return;
+    SASSERT(uncnstr(v));
+    SASSERT(to_app(v)->get_num_args() == 0);
+    m_mc->add(to_app(v)->get_decl(), def);
+}
+
+void iexpr_inverter::add_defs(unsigned num, expr* const* args, expr* u, expr* identity) {
+    expr_ref _id(identity, m);    
+    if (!m_mc)
+        return;
+    add_def(args[0], u);
+    for (unsigned i = 1; i < num; i++)
+        add_def(args[i], identity);
+}
+
+
+expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
+    auto* a = alloc(arith_expr_inverter, m);
+    auto* b = alloc(bv_expr_inverter, m);
+    auto* ar = alloc(array_expr_inverter, m, *this);
+    auto* dt = alloc(dt_expr_inverter, m);
+    m_inverters.setx(m.get_basic_family_id(), alloc(basic_expr_inverter, m), nullptr);
+    m_inverters.setx(a->get_fid(), a, nullptr);
+    m_inverters.setx(b->get_fid(), b, nullptr);
+    m_inverters.setx(ar->get_fid(), ar, nullptr);
+    m_inverters.setx(dt->get_fid(), dt, nullptr);
+}
+
+bool expr_inverter::is_converted(func_decl* f, unsigned num, expr* const* args) {
+    return false;
+}
+
+bool expr_inverter::operator()(func_decl* f, unsigned num, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) {
+    if (num == 0)
+        return false;
+            
+    for (unsigned i = 0; i < num; i++) 
+        if (!is_ground(args[i]))
+            return false;
+
+    family_id fid = f->get_family_id();
+    if (fid == null_family_id)
+        return false;
+            
+    if (is_converted(f, num, args))
+        return false;
+
+    auto* p = m_inverters.get(fid, nullptr);
+    return p && (*p)(f, num, args, new_expr, side_cond);       
+}
+
+bool expr_inverter::mk_diff(expr* t, expr_ref& r) {
+    sort * s = t->get_sort();
+    if (!m.is_fully_interp(s))
+        return false;
+
+    // If the interpreted sort has only one element,
+    // then it is unsound to eliminate the unconstrained variable in the equality
+    sort_size sz = s->get_num_elements();
+    if (sz.is_finite() && sz.size() <= 1)
+        return false;
+
+    if (!m_mc) {
+        // easy case, model generation is disabled.
+        mk_fresh_uncnstr_var_for(s, r);
+        return true;
+    }
+
+    family_id fid = s->get_family_id();
+    auto* p = m_inverters.get(fid, nullptr);
+    return p && p->mk_diff(t, r);
+}
+
+void expr_inverter::set_is_var(std::function<bool(expr*)>& is_var) {
+    for (auto* p : m_inverters)
+        if (p)
+            p->set_is_var(is_var);
+}
+
+void expr_inverter::set_model_converter(generic_model_converter* mc) {
+    for (auto* p : m_inverters)
+        if (p)
+            p->set_model_converter(mc);
+}
\ No newline at end of file
diff --git a/src/ast/converters/expr_inverter.h b/src/ast/converters/expr_inverter.h
new file mode 100644
index 000000000..1ca77dbab
--- /dev/null
+++ b/src/ast/converters/expr_inverter.h
@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    expr_inverter.h
+
+Abstract:
+
+    inverter interface and instance
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-11
+
+
+--*/
+#pragma once
+
+#include "ast/converters/generic_model_converter.h"
+
+class iexpr_inverter {
+protected:
+    ast_manager&                m;
+    std::function<bool(expr*)>  m_is_var;
+    generic_model_converter_ref m_mc;
+
+    bool uncnstr(expr* e) const { return m_is_var(e); }
+    bool uncnstr(unsigned num, expr * const * args) const;
+    void mk_fresh_uncnstr_var_for(sort* s, expr_ref& v);
+    void mk_fresh_uncnstr_var_for(func_decl* f, expr_ref& v) { mk_fresh_uncnstr_var_for(f->get_range(), v); }
+    void add_def(expr * v, expr * def);
+    void add_defs(unsigned num, expr * const * args, expr * u, expr * identity);
+
+public:
+    iexpr_inverter(ast_manager& m): m(m) {}
+    virtual ~iexpr_inverter() {}
+    virtual void set_is_var(std::function<bool(expr*)>& is_var) { m_is_var = is_var; }
+    virtual void set_model_converter(generic_model_converter* mc) { m_mc = mc; }
+    
+    virtual bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) = 0;
+    virtual bool mk_diff(expr* t, expr_ref& r) = 0;
+};
+
+class expr_inverter : public iexpr_inverter {
+    ptr_vector<iexpr_inverter> m_inverters;
+
+    bool is_converted(func_decl* f, unsigned num, expr* const* args);
+
+public:
+    expr_inverter(ast_manager& m);
+    ~expr_inverter() override;
+    bool operator()(func_decl* f, unsigned n, expr* const* args, expr_ref& new_expr, expr_ref& side_cond) override;
+    bool mk_diff(expr* t, expr_ref& r) override;
+    void set_is_var(std::function<bool(expr*)>& is_var) override; 
+    void set_model_converter(generic_model_converter* mc) override;
+};
diff --git a/src/ast/converters/generic_model_converter.h b/src/ast/converters/generic_model_converter.h
index c20bfebb3..85e8d0390 100644
--- a/src/ast/converters/generic_model_converter.h
+++ b/src/ast/converters/generic_model_converter.h
@@ -22,6 +22,7 @@ Notes:
 #include "ast/converters/model_converter.h"
 
 class generic_model_converter : public model_converter {
+public:
     enum instruction { HIDE, ADD };
     struct entry {
         func_decl_ref m_f;
@@ -30,6 +31,7 @@ class generic_model_converter : public model_converter {
         entry(func_decl* f, expr* d, ast_manager& m, instruction i):
             m_f(f, m), m_def(d, m), m_instruction(i) {}
     };
+private:
     ast_manager& m;
     std::string  m_orig;
     vector<entry> m_entries;
@@ -67,6 +69,8 @@ public:
     void set_env(ast_pp_util* visitor) override;
 
     void get_units(obj_map<expr, bool>& units) override;
+
+    vector<entry> const& entries() const { return m_entries; }
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;
diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp
index 0790b418d..1e7b6da3b 100644
--- a/src/ast/for_each_expr.cpp
+++ b/src/ast/for_each_expr.cpp
@@ -120,11 +120,11 @@ bool subterms::iterator::operator!=(iterator const& other) const {
 }
 
 
-subterms_postorder::subterms_postorder(expr_ref_vector const& es): m_es(es) {}
-subterms_postorder::subterms_postorder(expr_ref const& e) : m_es(e.m()) { if (e) m_es.push_back(e); }
+subterms_postorder::subterms_postorder(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {}
+subterms_postorder::subterms_postorder(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) { if (e) m_es.push_back(e); }
 subterms_postorder::iterator subterms_postorder::begin() { return iterator(*this, true); }
 subterms_postorder::iterator subterms_postorder::end() { return iterator(*this, false); }
-subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_es(f.m_es) {
+subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) {
     if (!start) m_es.reset();
     next();
 }
@@ -153,6 +153,13 @@ void subterms_postorder::iterator::next() {
                 }
             }
         }
+        else if (is_quantifier(e) && m_include_bound) {
+            expr* body = to_quantifier(e)->get_expr();
+            if (!m_visited.is_marked(body)) {
+                m_es.push_back(body);
+                all_visited = false;
+            }
+        }
         if (all_visited) {
             m_visited.mark(e, true);
             break;
diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h
index 99a0f6b9d..2d5ed05ae 100644
--- a/src/ast/for_each_expr.h
+++ b/src/ast/for_each_expr.h
@@ -200,9 +200,15 @@ public:
 };
 
 class subterms_postorder {
+    bool            m_include_bound;
     expr_ref_vector m_es;
+    subterms_postorder(expr_ref_vector const& es, bool include_bound);
+    subterms_postorder(expr_ref const& e, bool include_bound);
+    
+
 public:
     class iterator {
+        bool            m_include_bound = false;
         expr_ref_vector m_es;
         expr_mark       m_visited, m_seen; 
         void next();
@@ -214,8 +220,10 @@ public:
         bool operator==(iterator const& other) const;
         bool operator!=(iterator const& other) const;
     };
-    subterms_postorder(expr_ref_vector const& es);
-    subterms_postorder(expr_ref const& e);
+    static subterms_postorder all(expr_ref_vector const& es) { return subterms_postorder(es, true); }
+    static subterms_postorder ground(expr_ref_vector const& es) { return subterms_postorder(es, false); }
+    static subterms_postorder all(expr_ref const& e) { return subterms_postorder(e, true); }
+    static subterms_postorder ground(expr_ref const& e) { return subterms_postorder(e, false); }
     iterator begin();
     iterator end();
 };
diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt
index ef04cc433..75aa1ec7a 100644
--- a/src/ast/simplifiers/CMakeLists.txt
+++ b/src/ast/simplifiers/CMakeLists.txt
@@ -1,6 +1,7 @@
 z3_add_component(simplifiers
   SOURCES
     bv_slice.cpp
+    elim_unconstrained.cpp
     euf_completion.cpp
     extract_eqs.cpp
     model_reconstruction_trail.cpp
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
new file mode 100644
index 000000000..cbd575b6a
--- /dev/null
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -0,0 +1,297 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    elim_unconstrained.cpp
+
+Abstract:
+
+   Incremental, modular and more efficient version of elim_unconstr_tactic and 
+   reduce_invertible_tactic.
+
+   reduce_invertible_tactic should be subsumed by elim_unconstr_tactic
+   elim_unconstr_tactic has some built-in limitations that are not easy to fix with small changes:
+   - it is inefficient for examples like x <= y, y <= z, z <= u, ...
+     All variables x, y, z, .. can eventually be eliminated, but the tactic requires a global 
+     analysis between each elimination. We address this by using reference counts and maintaining
+     a heap of reference counts.
+   - it does not accomodate side constraints. The more general invertibility reduction methods, such 
+     as those introduced for bit-vectors use side constraints.
+   - it is not modular: we detach the expression invertion routines to self-contained code.
+
+   Maintain a representation of terms as a set of nodes.
+   Each node has:
+
+   - reference count = number of parents that are live
+   - orig - original term, the orig->get_id() is the index to the node
+   - term - current term representing the node after rewriting
+   - parents - list of parents where orig occurs.
+
+  Subterms have reference counts
+  Elegible variables are inserted into a heap ordered by reference counts.
+  Variables that have reference count 1 are examined for invertibility.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-11.
+
+--*/
+
+
+
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/recfun_decl_plugin.h"
+#include "ast/simplifiers/elim_unconstrained.h"
+
+elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
+    dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) {
+
+    std::function<bool(expr*)> is_var = [&](expr* e) {
+        return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount == 1;
+    };
+
+    m_inverter.set_is_var(is_var);
+}
+
+
+void elim_unconstrained::eliminate() {
+
+    while (!m_heap.empty()) {
+        expr_ref r(m), side_cond(m);
+        int v = m_heap.erase_min();
+        node& n = get_node(v);
+        IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
+        if (n.m_refcount == 0)
+            continue;
+        if (n.m_refcount > 1)
+            return;
+
+        if (n.m_parents.empty())
+            continue;
+        expr* e = get_parent(v);
+        for (expr* p : n.m_parents)
+            IF_VERBOSE(11, verbose_stream() << "parent " << mk_pp(p, m) << "\n");
+        if (!is_app(e))
+            continue;
+        if (!is_ground(e))
+            continue;
+        app* t = to_app(e);
+        m_args.reset();
+        for (expr* arg : *to_app(t))
+            m_args.push_back(get_node(arg).m_term);
+        if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond))
+            continue;
+
+        m_stats.m_num_eliminated++;
+        n.m_refcount = 0;
+        SASSERT(r);
+        m_trail.push_back(r);
+        gc(e);
+
+        get_node(e).m_term = r;
+        get_node(e).m_refcount++;
+        IF_VERBOSE(11, verbose_stream() << mk_pp(e, m) << "\n");
+        SASSERT(!m_heap.contains(e->get_id()));
+        if (is_uninterp_const(r)) 
+            m_heap.insert(e->get_id());                    
+
+        IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " " << mk_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n");
+
+        SASSERT(!side_cond && "not implemented to add side conditions\n");
+    }
+}
+
+void elim_unconstrained::add_term(expr* t) {
+    expr_ref_vector terms(m);
+    terms.push_back(t);
+    init_terms(terms);
+}
+
+expr* elim_unconstrained::get_parent(unsigned n) const {
+    for (expr* p : get_node(n).m_parents)
+        if (get_node(p).m_refcount > 0 && get_node(p).m_term == get_node(p).m_orig)
+            return p;
+    IF_VERBOSE(0, verbose_stream() << "term " << mk_pp(get_node(n).m_term, m) << "\n");
+    for (expr* p : get_node(n).m_parents)
+        IF_VERBOSE(0, verbose_stream() << "parent " << mk_pp(p, m) << "\n");
+    UNREACHABLE();
+    return nullptr;
+}
+/**
+ * initialize node structure
+ */
+void elim_unconstrained::init_nodes() {
+    expr_ref_vector terms(m);
+    for (unsigned i = 0; i < m_fmls.size(); ++i)
+        terms.push_back(m_fmls[i].fml());
+    m_trail.append(terms);
+    m_heap.reset();
+
+    init_terms(terms);
+
+    for (expr* e : terms)
+        inc_ref(e);
+
+    // freeze subterms before the head.
+    terms.reset();
+    for (unsigned i = 0; i < m_qhead; ++i)
+        terms.push_back(m_fmls[i].fml());
+    for (expr* e : subterms::all(terms))
+        m_frozen.mark(e, true);    
+
+    
+    recfun::util rec(m);
+    if (rec.has_rec_defs()) {
+        for (func_decl* f : rec.get_rec_funs()) {
+            expr* rhs = rec.get_def(f).get_rhs();
+            for (expr* t : subterms::all(expr_ref(rhs, m)))
+                m_frozen.mark(t);
+        }
+    }
+}
+
+void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
+    unsigned max_id = 0;
+    for (expr* e : subterms::all(terms))
+        max_id = std::max(max_id, e->get_id());
+
+    m_nodes.reserve(max_id + 1);
+    m_heap.reserve(max_id + 1);
+
+    for (expr* e : subterms_postorder::all(terms)) {
+        node& n = get_node(e);
+        if (n.m_term)
+            continue;
+        n.m_orig = e;
+        n.m_term = e;
+        n.m_refcount = 0;
+        if (is_uninterp_const(e))
+            m_heap.insert(e->get_id());
+        if (is_quantifier(e)) {
+            expr* body = to_quantifier(e)->get_expr();
+            get_node(body).m_parents.push_back(e);
+            inc_ref(body);
+        }
+        else if (is_app(e)) {
+            for (expr* arg : *to_app(e)) {
+                get_node(arg).m_parents.push_back(e);
+                inc_ref(arg);
+            }
+        }
+    }
+}
+
+void elim_unconstrained::gc(expr* t) {
+    ptr_vector<expr> todo;
+    todo.push_back(t);
+    while (!todo.empty()) {
+        t = todo.back();
+        todo.pop_back();
+        node& n = get_node(t);  
+        if (n.m_refcount == 0)
+            continue;
+        dec_ref(t);
+        if (n.m_refcount != 0)
+            continue;
+        if (is_app(t)) {
+            for (expr* arg : *to_app(t))
+                todo.push_back(arg);
+        }
+        else if (is_quantifier(t)) 
+            todo.push_back(to_quantifier(t)->get_expr());        
+    }
+}
+
+/**
+ * walk nodes starting from lowest depth and reconstruct their normalized forms.
+ */
+void elim_unconstrained::reconstruct_terms() {
+    expr_ref_vector terms(m);
+    for (unsigned i = m_qhead; i < m_fmls.size(); ++i)
+        terms.push_back(m_fmls[i].fml());    
+
+    for (expr* e : subterms_postorder::all(terms)) {
+        node& n = get_node(e);
+        expr* t = n.m_term;
+        if (t != n.m_orig)
+            continue;
+        if (is_app(t)) {
+            bool change = false;
+            m_args.reset();
+            for (expr* arg : *to_app(t)) {
+                node& n2 = get_node(arg);
+                m_args.push_back(n2.m_term);
+                change |= n2.m_term != n2.m_orig;
+            }
+            if (change) {
+                n.m_term = m.mk_app(to_app(t)->get_decl(), m_args);
+                m_trail.push_back(n.m_term);
+            }            
+        }
+        else if (is_quantifier(t)) {
+            node& n2 = get_node(to_quantifier(t)->get_expr());
+            if (n2.m_term != n2.m_orig) {
+                n.m_term = m.update_quantifier(to_quantifier(t), n2.m_term);
+                m_trail.push_back(n.m_term);
+            }
+        }
+    }
+}
+
+void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
+    for (unsigned i = m_qhead; i < m_fmls.size(); ++i) {
+        auto [f, d] = m_fmls[i]();
+        node& n = get_node(f);
+        expr* g = n.m_term;
+        if (f == g)
+            continue;
+        old_fmls.push_back(m_fmls[i]);
+        m_fmls.update(i, dependent_expr(m, g, d));
+        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
+        TRACE("elim_unconstrained", tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
+    }
+}
+
+void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls) {
+    auto& trail = m_fmls.model_trail();
+    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
+    scoped_ptr<expr_substitution> sub = alloc(expr_substitution, m, true, false);
+    rp->set_substitution(sub.get());
+    expr_ref new_def(m);
+    for (auto const& entry : mc.entries()) {
+        switch (entry.m_instruction) {
+        case generic_model_converter::instruction::HIDE:
+            break;
+        case generic_model_converter::instruction::ADD:
+            new_def = entry.m_def;
+            (*rp)(new_def);           
+            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
+            break;
+        }
+    }
+    trail.push(sub.detach(), old_fmls);
+
+    for (auto const& entry : mc.entries()) {
+        switch (entry.m_instruction) {
+        case generic_model_converter::instruction::HIDE:
+            trail.push(entry.m_f);
+            break;
+        case generic_model_converter::instruction::ADD:
+            break;
+        }
+    }
+}
+
+void elim_unconstrained::reduce() {
+    generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
+    m_inverter.set_model_converter(mc.get());
+    init_nodes();
+    eliminate();
+    reconstruct_terms();
+    vector<dependent_expr> old_fmls;
+    assert_normalized(old_fmls);
+    update_model_trail(*mc, old_fmls);
+    advance_qhead(m_fmls.size());
+}
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
new file mode 100644
index 000000000..327ceeff0
--- /dev/null
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    elim_unconstrained.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-2.
+
+--*/
+
+
+#pragma once
+
+#include "util/heap.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/converters/expr_inverter.h"
+
+
+class elim_unconstrained : public dependent_expr_simplifier {
+
+    struct node {
+        unsigned         m_refcount;
+        expr*            m_term;
+        expr*            m_orig;
+        ptr_vector<expr> m_parents;
+    };
+    struct var_lt {
+        elim_unconstrained& s;
+        var_lt(elim_unconstrained& s) : s(s) {}
+        bool operator()(int v1, int v2) const {
+            return s.get_node(v1).m_refcount < s.get_node(v2).m_refcount;
+        }
+    };
+    struct stats {
+        unsigned m_num_eliminated = 0;
+        void reset() { m_num_eliminated = 0; }
+    };
+    expr_inverter            m_inverter;
+    vector<node>             m_nodes;
+    var_lt                   m_lt;
+    heap<var_lt>             m_heap;
+    expr_ref_vector          m_trail;
+    ptr_vector<expr>         m_args;
+    expr_mark                m_frozen;
+    stats                    m_stats;
+
+    bool operator()(int v1, int v2) const { return get_node(v1).m_refcount < get_node(v2).m_refcount; }
+
+    node& get_node(unsigned n) { return m_nodes[n]; }
+    node const& get_node(unsigned n) const { return m_nodes[n]; }
+    node& get_node(expr* t) { return m_nodes[t->get_id()]; }
+    node const& get_node(expr* t) const { return m_nodes[t->get_id()]; }
+    unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; }
+    void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
+    void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
+    void gc(expr* t);
+
+    expr* get_parent(unsigned n) const;
+    void init_refcounts();
+    void dec_refcounts(expr* t);
+
+    void add_term(expr* t);
+    void init_terms(expr_ref_vector const& terms);
+
+    void init_nodes();
+    void eliminate();
+    void reconstruct_terms();
+    void assert_normalized(vector<dependent_expr>& old_fmls);
+    void update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls);
+    
+public:
+
+    elim_unconstrained(ast_manager& m, dependent_expr_state& fmls);
+
+    void reduce() override;
+
+    void collect_statistics(statistics& st) const override { st.update("elim-unconstr", m_stats.m_num_eliminated); }
+
+    void reset_statistics() override { m_stats.reset(); }
+};
diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 373a500bf..a5f1cf8b0 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -30,6 +30,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
         if (!t->m_active)
             continue;
 
+        if (t->m_hide)
+            continue;
+        
         // updates that have no intersections with current variables are skipped
         if (!t->intersects(free_vars)) 
             continue;        
@@ -79,6 +82,11 @@ model_converter_ref model_reconstruction_trail::get_model_converter() {
         if (!t->m_active)
             continue;
 
+        if (t->m_hide) {
+            mc->hide(t->m_hide);
+            continue;
+        }
+
         if (first) {
             first = false;
             for (auto const& [v, def] : t->m_subst->sub()) {
diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h
index c9b42bc92..eeef136ee 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.h
+++ b/src/ast/simplifiers/model_reconstruction_trail.h
@@ -35,11 +35,14 @@ class model_reconstruction_trail {
     struct entry {
         scoped_ptr<expr_substitution> m_subst;
         vector<dependent_expr>        m_removed;
+        func_decl*                    m_hide = nullptr;
         bool                          m_active = true;
 
         entry(expr_substitution* s, vector<dependent_expr> const& rem) :
             m_subst(s), m_removed(rem) {}
 
+        entry(func_decl* h) : m_hide(h) {}
+
         bool is_loose() const { return !m_removed.empty(); }
 
         bool intersects(ast_mark const& free_vars) const {
@@ -48,8 +51,6 @@ class model_reconstruction_trail {
                     return true;
             return false;
         }
-
-
     };
 
     ast_manager&             m;
@@ -81,6 +82,14 @@ public:
     */
     void push(expr_substitution* s, vector<dependent_expr> const& removed) {
         m_trail.push_back(alloc(entry, s, removed));
+        m_trail_stack.push(push_back_vector(m_trail));       
+    }
+
+    /**
+    * add declaration to hide
+    */
+    void push(func_decl* f) {
+        m_trail.push_back(alloc(entry, f));
         m_trail_stack.push(push_back_vector(m_trail));
     }
 
diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt
index 38d2699f0..bab61afce 100644
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@@ -17,7 +17,6 @@ z3_add_component(core_tactics
     pb_preprocess_tactic.cpp
     propagate_values_tactic.cpp
     reduce_args_tactic.cpp
-    reduce_invertible_tactic.cpp
     simplify_tactic.cpp
     solve_eqs_tactic.cpp
     special_relations_tactic.cpp
@@ -39,6 +38,7 @@ z3_add_component(core_tactics
     dom_simplify_tactic.h
     elim_term_ite_tactic.h
     elim_uncnstr_tactic.h
+    elim_uncnstr2_tactic.h
     euf_completion_tactic.h
     injectivity_tactic.h
     nnf_tactic.h
@@ -46,7 +46,6 @@ z3_add_component(core_tactics
     pb_preprocess_tactic.h
     propagate_values_tactic.h
     reduce_args_tactic.h
-    reduce_invertible_tactic.h
     simplify_tactic.h
     solve_eqs_tactic.h
     solve_eqs2_tactic.h
diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h
new file mode 100644
index 000000000..2c5f81d5e
--- /dev/null
+++ b/src/tactic/core/elim_uncnstr2_tactic.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    elim_unconstr2_tactic.h
+
+Abstract:
+
+    Tactic for eliminating unconstrained terms.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-30
+
+--*/
+#pragma once
+
+#include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/elim_unconstrained.h"
+#include "ast/simplifiers/elim_unconstrained.h"
+
+class elim_uncnstr2_tactic_factory : public dependent_expr_simplifier_factory {
+public:
+    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
+        return alloc(elim_unconstrained, m, s);
+    }
+};
+
+inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory), "elim-unconstr2");
+}
+
+
+/*
+  ADD_TACTIC("elim-uncnstr2", "eliminate unconstrained variables.", "mk_elim_uncnstr2_tactic(m, p)")
+*/
+
+
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 34aa748d9..5f0963bfd 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -856,9 +856,8 @@ class elim_uncnstr_tactic : public tactic {
     
     void init_mc(bool produce_models) {
         m_mc = nullptr;
-        if (produce_models) {
-            m_mc = alloc(mc, m(), "elim_uncstr");
-        }
+        if (produce_models) 
+            m_mc = alloc(mc, m(), "elim_uncstr");        
     }
     
     void init_rw(bool produce_proofs) {
@@ -872,7 +871,7 @@ class elim_uncnstr_tactic : public tactic {
         m_vars.reset();
         collect_occs p;
         p(*g, m_vars);
-        if (m_vars.empty() || recfun::util(m()).has_defs()) {
+        if (m_vars.empty() || recfun::util(m()).has_rec_defs()) {
             result.push_back(g.get());
             // did not increase depth since it didn't do anything.
             return;
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
deleted file mode 100644
index ba9b5d752..000000000
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ /dev/null
@@ -1,576 +0,0 @@
-/*++
-Copyright (c) 2018 Microsoft Corporation
-
-Module Name:
-
-    reduce_invertible_tactic.cpp
-
-Abstract:
-
-    Reduce invertible variables.
-
-Author:
-
-    Nuno Lopes (nlopes)         2018-6-30
-    Nikolaj Bjorner (nbjorner)
-
-Notes:
-
- 1. Walk through top-level uninterpreted constants.
-
---*/
-
-#include "ast/bv_decl_plugin.h"
-#include "ast/arith_decl_plugin.h"
-#include "ast/ast_pp.h"
-#include "ast/rewriter/expr_safe_replace.h"
-#include "ast/rewriter/rewriter_def.h"
-#include "ast/rewriter/th_rewriter.h"
-#include "tactic/tactic.h"
-#include "tactic/core/reduce_invertible_tactic.h"
-#include "tactic/core/collect_occs.h"
-#include "ast/converters/generic_model_converter.h"
-#include <cstdint>
-
-namespace {
-class reduce_invertible_tactic : public tactic {
-    ast_manager& m;
-    bv_util      m_bv;
-    arith_util   m_arith;
-
-public:
-    reduce_invertible_tactic(ast_manager & m):
-        m(m),
-        m_bv(m),
-        m_arith(m)
-    {}
-
-    char const* name() const override { return "reduce_invertible"; }
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(reduce_invertible_tactic, m);
-    }
-    
-    void operator()(goal_ref const & g, goal_ref_buffer & result) override {
-        tactic_report report("reduce-invertible", *g);
-        bool change = true;
-        while (change) {
-            change = false;
-            m_inverted.reset();
-            m_parents.reset();
-            collect_parents(g);
-            collect_occs occs;
-            obj_hashtable<expr> vars;
-            generic_model_converter_ref mc;
-            occs(*g, vars);
-            expr_safe_replace sub(m);
-            expr_ref new_v(m);
-            expr * p;
-            for (expr* v : vars) {
-                if (is_invertible(v, p, new_v, &mc)) {
-                    mark_inverted(p);
-                    sub.insert(p, new_v);
-                    TRACE("invertible_tactic", tout << mk_pp(p, m) << " " << new_v << "\n";);
-                    change = true;
-                    break;
-                }
-            }
-            reduce_q_rw rw(*this);
-            unsigned sz = g->size();
-            for (unsigned idx = 0; !g->inconsistent() && idx < sz; idx++) {
-                checkpoint();
-                expr* f = g->form(idx);
-                expr_ref f_new(m);
-                sub(f, f_new);
-                rw(f_new, f_new);
-                if (f == f_new) continue;
-                proof_ref new_pr(m);
-                if (g->proofs_enabled()) {
-                    proof * pr = g->pr(idx);
-                    new_pr     = m.mk_rewrite(f, f_new);
-                    new_pr     = m.mk_modus_ponens(pr, new_pr);
-                }
-                g->update(idx, f_new, new_pr, g->dep(idx));
-            }  
-            if (mc) g->add(mc.get());
-	    TRACE("invertible_tactic", g->display(tout););
-	    g->inc_depth();
-        }        
-        result.push_back(g.get());
-	CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
-    }
-
-    void cleanup() override {}
-
-private:
-    void checkpoint() { 
-        tactic::checkpoint(m);
-    }
-
-    bool is_bv_neg(expr * e) {
-        if (m_bv.is_bv_neg(e))
-            return true;
-
-        expr *a, *b;
-        if (m_bv.is_bv_mul(e, a, b)) {
-            return m_bv.is_allone(a) || m_bv.is_allone(b);
-        }
-        return false;
-    }
-
-    expr_mark        m_inverted;
-    void mark_inverted(expr *p) {
-        ptr_buffer<expr> todo;
-        todo.push_back(p);
-        while (!todo.empty()) {
-            p = todo.back();
-            todo.pop_back();
-            if (!m_inverted.is_marked(p)) {
-                m_inverted.mark(p, true);
-                if (is_app(p)) {
-                    for (expr* arg : *to_app(p)) {
-                        todo.push_back(arg);
-                    }
-                }
-                else if (is_quantifier(p)) {
-                    todo.push_back(to_quantifier(p)->get_expr());
-                }
-            }
-        }
-    }
-
-    // store one parent of expression, or null if multiple
-    struct parents {
-        parents(): m_p(0) {}
-        uintptr_t m_p;
-
-        void set(expr * e) {
-            SASSERT((uintptr_t)e != 1);
-            if (!m_p) m_p = (uintptr_t)e;
-            else m_p = 1;
-        }
-
-        expr * get() const {
-          return m_p == 1 ? nullptr : (expr*)m_p;
-        }
-    };
-    svector<parents> m_parents;
-    struct parent_collector {
-        reduce_invertible_tactic& c;
-        parent_collector(reduce_invertible_tactic& c):c(c) {}
-        void operator()(app* n) {
-            for (expr* arg : *n) {
-                c.m_parents.reserve(arg->get_id() + 1);
-                c.m_parents[arg->get_id()].set(n);
-            }
-        }
-
-        void operator()(var* v) {
-            c.m_parents.reserve(v->get_id() + 1);
-        }
-
-        void operator()(quantifier* q) {}
-    };
-
-    void collect_parents(goal_ref const& g) {
-        parent_collector proc(*this);
-        expr_fast_mark1 visited;
-        unsigned sz = g->size();
-        for (unsigned i = 0; i < sz; i++) {
-            checkpoint();
-            quick_for_each_expr(proc, visited, g->form(i));
-        }        
-    }    
-
-    void ensure_mc(generic_model_converter_ref* mc) {
-        if (mc && !(*mc)) *mc = alloc(generic_model_converter, m, "reduce-invertible");        
-    }
-
-    bool is_full_domain_var(expr* v, rational& model) {
-        auto f = is_app(v) ? to_app(v)->get_decl() : nullptr;
-        if (!f || f->get_family_id() != m_bv.get_family_id() || f->get_arity() == 0)
-            return false;
-
-        switch (f->get_decl_kind()) {
-        case OP_BADD:
-        case OP_BSUB:
-            model = rational::zero();
-            return true;
-
-        case OP_BAND:
-            model = rational::power_of_two(m_bv.get_bv_size(v)) - rational::one();
-            return true;
-
-        case OP_BMUL:
-            model = rational::one();
-            return true;
-
-        case OP_BSDIV:
-        case OP_BSDIV0:
-        case OP_BSDIV_I:
-        case OP_BUDIV:
-        case OP_BUDIV0:
-        case OP_BUDIV_I:
-        default:
-            return false;
-        }
-    }
-
-    bool rewrite_unconstr(expr* v, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var) {
-        rational mdl;
-        if (!is_full_domain_var(v, mdl))
-            return false;
-
-        rational r;
-        app* a = to_app(v);
-        expr* fst_arg = a->get_arg(0);
-
-        for (expr* arg : *a) 
-            if (!m_parents[arg->get_id()].get())
-                return false;
-
-        if (is_var(fst_arg)) {
-            for (expr* arg : *a) {
-                if (!is_var(arg))
-                    return false;
-                if (to_var(arg)->get_idx() >= max_var)
-                    return false;
-            }
-        }
-        else {            
-            if (!is_uninterp_const(fst_arg))
-                return false;
-            bool first = true;
-            for (expr* arg : *a) {
-                if (!is_app(arg))
-                    return false;
-                if (is_uninterp_const(arg))
-                    continue;
-                if (m_bv.is_numeral(arg, r) && r == mdl) {
-                    if (first || mdl.is_zero()) {
-                        first = false;
-                        continue;
-                    }
-                    else
-                        return false;
-                }
-                return false;
-            }
-        }
-
-        if (mc) {
-            ensure_mc(mc);
-            expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m);
-            for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
-                expr* arg = a->get_arg(i);
-                if (m_bv.is_numeral(arg))
-                    continue;
-                (*mc)->add(arg, num);
-            }
-        }
-        new_v = fst_arg;
-        return true;
-    }
-
-    // TBD: could be made to be recursive, by walking multiple layers of parents.
-    
-    bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
-        rational r;
-        if (m_parents.size() <= v->get_id()) {
-            return false;
-        }
-        p = m_parents[v->get_id()].get();
-        if (!p || m_inverted.is_marked(p) || (mc && !is_ground(p))) {
-            return false;
-        }
-
-        if (m_bv.is_bv_xor(p) ||
-            m_bv.is_bv_not(p) ||
-            is_bv_neg(p)) {
-            if (mc) {
-                ensure_mc(mc);
-                (*mc)->add(v, p);
-            }
-            new_v = v;
-            return true;
-        }
-
-        if (rewrite_unconstr(p, new_v, mc, max_var))
-            return true;
-
-        if (m_bv.is_bv_add(p)) {
-            if (mc) {
-                ensure_mc(mc);
-                // if we solve for v' := v + t
-                // then the value for v is v' - t
-                expr_ref def(v, m);
-                for (expr* arg : *to_app(p)) {
-                    if (arg != v) def = m_bv.mk_bv_sub(def, arg);
-                }
-                (*mc)->add(v, def);
-            }
-            new_v = v;
-            return true;
-        }
-
-        if (m_bv.is_bv_mul(p)) {
-            expr_ref rest(m);
-            for (expr* arg : *to_app(p)) {
-                if (arg != v) { 
-                    if (rest) 
-                        rest = m_bv.mk_bv_mul(rest, arg);
-                    else
-                        rest = arg;
-                }
-            }
-            if (!rest) return false;
-
-            // so far just support numeral
-            if (!m_bv.is_numeral(rest, r)) 
-                return false;
-
-            // create case split on
-            // divisbility of 2
-            // v * t -> 
-            // if t = 0, set v' := 0 and the solution for v is 0.
-            // otherwise,
-            // let i be the position of the least bit of t set to 1
-            // then extract[sz-1:i](v) ++ zero[i-1:0] is the invertible of v * t
-            // thus
-            //    extract[i+1:0](t) = 1 ++ zero[i-1:0] -> extract[sz-1:i](v) ++ zero[i-1:0]
-            // to reproduce the original v from t
-            // solve for v*t = extract[sz-1:i](v') ++ zero[i-1:0]
-            // using values for t and v'
-            // thus let t' = t / 2^i
-            // and t'' = the multiplicative inverse of t'
-            // then t'' * v' * t = t'' * v' * t' * 2^i = v' * 2^i = extract[sz-1:i](v') ++ zero[i-1:0]
-            // so t'' *v' works 
-            // 
-            unsigned sz = m_bv.get_bv_size(p);
-            expr_ref bit1(m_bv.mk_numeral(1, 1), m);
-
-            
-            unsigned sh = 0;
-            while (r.is_pos() && r.is_even()) {
-                r /= rational(2);
-                ++sh;
-            }
-            if (r.is_pos() && sh > 0) 
-                new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh));
-            else
-                new_v = v;
-            if (mc && !r.is_zero()) {
-                ensure_mc(mc);
-                expr_ref def(m);
-                rational inv_r;
-                VERIFY(r.mult_inverse(sz, inv_r));
-                def = m_bv.mk_bv_mul(m_bv.mk_numeral(inv_r, sz), v);
-                (*mc)->add(v, def);
-                TRACE("invertible_tactic", tout << def << "\n";);
-            }
-            return true;
-        }
-        if (m_bv.is_bv_sub(p)) {
-            // TBD
-        }
-        if (m_bv.is_bv_udivi(p)) {
-            // TBD
-        }
-        // sdivi, sremi, uremi, smodi
-        // TBD
-
-        if (m_arith.is_mul(p) && m_arith.is_real(p)) {
-            expr_ref rest(m);
-            for (expr* arg : *to_app(p)) {
-                if (arg != v) {
-                    if (rest) 
-                        rest = m_arith.mk_mul(rest, arg);
-                    else
-                        rest = arg;
-                }
-            }
-            if (!rest) return false;
-            if (!m_arith.is_numeral(rest, r) || r.is_zero())
-                return false;
-            expr_ref zero(m_arith.mk_real(0), m);
-            new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v);
-            if (mc) {
-                ensure_mc(mc);
-                expr_ref def(m_arith.mk_div(v, rest), m);
-                (*mc)->add(v, def);
-            }
-            return true;        
-        }
-
-
-        expr* e1 = nullptr, *e2 = nullptr;
-        
-        // v / t unless t != 0
-        if (m_arith.is_div(p, e1, e2) && e1 == v && m_arith.is_numeral(e2, r) && !r.is_zero()) {
-            new_v = v;
-            if (mc) {
-                ensure_mc(mc);
-                (*mc)->add(v, m_arith.mk_mul(e1, e2));
-            }
-            return true;
-        }
-       
-        if (m.is_eq(p, e1, e2)) {
-            TRACE("invertible_tactic", tout << mk_pp(v, m) << "\n";);
-            if (mc && has_diagonal(e1)) {
-                ensure_mc(mc);
-                new_v = m.mk_fresh_const("eq", m.mk_bool_sort());
-                SASSERT(v == e1 || v == e2);
-                expr* other = (v == e1) ? e2 : e1;
-                (*mc)->hide(new_v);
-                (*mc)->add(v, m.mk_ite(new_v, other, mk_diagonal(other)));
-                return true;
-            }
-            else if (mc) {
-                // diagonal functions for other types depend on theory.
-                return false;
-            }
-            else if (is_var(v) && is_non_singleton_sort(v->get_sort())) {
-                new_v = m.mk_var(to_var(v)->get_idx(), m.mk_bool_sort());
-                return true;
-            }
-        }
-
-        //
-        // v <= u
-        // => u + 1 == 0 or delta
-        // v := delta ? u : u + 1
-        //
-        if (m_bv.is_bv_ule(p, e1, e2) && e1 == v && mc) {
-            ensure_mc(mc);
-            unsigned sz = m_bv.get_bv_size(e2);
-            expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
-            expr_ref succ_e2(m_bv.mk_bv_add(e2, m_bv.mk_numeral(1, sz)), m);
-            new_v = m.mk_or(delta, m.mk_eq(succ_e2, m_bv.mk_numeral(0, sz)));
-            (*mc)->hide(delta);
-            (*mc)->add(v, m.mk_ite(delta, e2, succ_e2));
-            return true;
-        }
-
-        //
-        // u <= v
-        // => u == 0 or delta
-        // v := delta ? u : u - 1
-        //
-        if (m_bv.is_bv_ule(p, e1, e2) && e2 == v && mc) {
-            ensure_mc(mc);
-            unsigned sz = m_bv.get_bv_size(e1);
-            expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m);
-            expr_ref pred_e1(m_bv.mk_bv_sub(e1, m_bv.mk_numeral(1, sz)), m);
-            new_v = m.mk_or(delta, m.mk_eq(e1, m_bv.mk_numeral(0, sz)));
-            (*mc)->hide(delta);
-            (*mc)->add(v, m.mk_ite(delta, e1, pred_e1));
-            return true;
-        }
-        return false;
-    }
-
-    bool has_diagonal(expr* e) {
-        return 
-            m_bv.is_bv(e) ||
-            m.is_bool(e) ||
-            m_arith.is_int_real(e);
-    }
-
-    expr * mk_diagonal(expr* e) {
-        if (m_bv.is_bv(e)) return m_bv.mk_bv_not(e);
-        if (m.is_bool(e)) return m.mk_not(e);
-        if (m_arith.is_int(e)) return m_arith.mk_add(m_arith.mk_int(1), e);
-        if (m_arith.is_real(e)) return m_arith.mk_add(m_arith.mk_real(1), e);
-        UNREACHABLE();
-        return e;
-    }
-
-    bool is_non_singleton_sort(sort* s) {
-        if (m.is_uninterp(s)) return false;
-        sort_size sz = s->get_num_elements();
-        if (sz.is_finite() && sz.size() == 1) return false;
-        return true;
-    }
-
-    struct reduce_q_rw_cfg : public default_rewriter_cfg {
-        ast_manager&              m;
-        reduce_invertible_tactic& t;
-
-        reduce_q_rw_cfg(reduce_invertible_tactic& t): m(t.m), t(t) {}
-        
-        bool reduce_quantifier(quantifier * old_q, 
-                               expr * new_body, 
-                               expr * const * new_patterns, 
-                               expr * const * new_no_patterns,
-                               expr_ref & result,
-                               proof_ref & result_pr) {
-            if (is_lambda(old_q)) return false;
-            if (has_quantifiers(new_body)) return false;
-            ref_buffer<var, ast_manager> vars(m);
-            ptr_buffer<sort> new_sorts;
-            unsigned n = old_q->get_num_decls();
-            for (unsigned i = 0; i < n; ++i) {
-                sort* srt = old_q->get_decl_sort(i);
-                vars.push_back(m.mk_var(n - i - 1, srt));
-                new_sorts.push_back(srt);
-            }
-            // for each variable, collect parents,
-            // ensure they are in unique location and not under other quantifiers.
-            // if they are invertible, then produce inverting expression.
-            //
-            expr_safe_replace sub(m);
-            t.m_parents.reset();
-            t.m_inverted.reset();
-            expr_ref new_v(m);
-            expr * p;
-            
-            {
-                parent_collector proc(t);           
-                expr_fast_mark1 visited;
-                quick_for_each_expr(proc, visited, new_body);
-            }
-            bool has_new_var = false;
-            for (unsigned i = 0; i < vars.size(); ++i) {
-                var* v = vars[i];
-                if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr, vars.size())) {
-                    TRACE("invertible_tactic", tout << mk_pp(v, m) << " " << mk_pp(p, m) << "\n";);
-                    t.mark_inverted(p);
-                    sub.insert(p, new_v);
-                    new_sorts[i] = new_v->get_sort();
-                    has_new_var |= new_v != v;
-                }
-            }
-            if (has_new_var) {
-                sub(new_body, result);
-                result = m.mk_quantifier(old_q->get_kind(), new_sorts.size(), new_sorts.data(), old_q->get_decl_names(), result, old_q->get_weight());
-                result_pr = nullptr;
-                return true;
-            }
-            if (!sub.empty()) {
-                sub(new_body, result);
-                result = m.update_quantifier(old_q,  old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns, result);
-                result_pr = nullptr;
-                return true;
-            }
-            return false;
-        }
-
-        bool occurs_under_nested_q(var* v, expr* body) {
-            return has_quantifiers(body);
-        }
-    };
-
-    struct reduce_q_rw : rewriter_tpl<reduce_q_rw_cfg> {
-        reduce_q_rw_cfg m_cfg;
-    public:
-        reduce_q_rw(reduce_invertible_tactic& t):
-            rewriter_tpl<reduce_q_rw_cfg>(t.m, false, m_cfg),
-            m_cfg(t) {}
-    };
-};
-}
-
-tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const &) {
-    return alloc(reduce_invertible_tactic, m);
-}
diff --git a/src/tactic/core/reduce_invertible_tactic.h b/src/tactic/core/reduce_invertible_tactic.h
deleted file mode 100644
index d40bf8a59..000000000
--- a/src/tactic/core/reduce_invertible_tactic.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/*++
-Copyright (c) 2018 Microsoft Corporation
-
-Module Name:
-
-    reduce_invertible_tactic.h
-
-Abstract:
-
-    Reduce invertible variables.
-
-Author:
-
-    Nuno Lopes (nlopes)         2018-6-30
-    Nikolaj Bjorner (nbjorner)
-
-Notes:
-
---*/
-
-#pragma once
-#include "util/params.h"
-
-class tactic;
-class ast_manager;
-
-tactic * mk_reduce_invertible_tactic(ast_manager & m, params_ref const & p = params_ref());
-
-/*
-  ADD_TACTIC("reduce-invertible", "reduce invertible variable occurrences.", "mk_reduce_invertible_tactic(m, p)")
-*/
-
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 56e27ee9a..419037839 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -15,6 +15,7 @@ Author:
     Nikolaj Bjorner (nbjorner) 2022-11-2.
 
 --*/
+#pragma once
 #include "tactic/tactic.h"
 #include "ast/simplifiers/dependent_expr_state.h"