diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 7f351ecb6..7822a370c 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -4,6 +4,7 @@ z3_add_component(rewriter
     array_rewriter.cpp
     ast_counter.cpp
     bit2int.cpp
+    bv2int_translator.cpp
     bool_rewriter.cpp
     bv_bounds.cpp
     bv_elim.cpp
diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
new file mode 100644
index 000000000..77a4a1d76
--- /dev/null
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -0,0 +1,680 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv2int_translator
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-27
+
+--*/
+
+#include "ast/ast.h"
+#include "ast/arith_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
+#include "ast/rewriter/bv2int_translator.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
+
+bv2int_translator::bv2int_translator(ast_manager& m, bv2int_translator_trail& ctx) :
+    m(m),
+    ctx(ctx),
+    bv(m),
+    a(m),
+    m_translate(m),
+    m_args(m),
+    m_pinned(m),
+    m_vars(m),
+    m_preds(m)
+{}
+
+void bv2int_translator::reset(bool is_plugin) {
+    m_vars.reset();
+    m_preds.reset();
+    for (unsigned i = m_translate.size(); i-- > 0; )
+        m_translate[i] = nullptr;
+    m_is_plugin = is_plugin;
+}
+
+
+void bv2int_translator::set_translated(expr* e, expr* r) {
+    SASSERT(r);
+    SASSERT(!is_translated(e));
+    m_translate.setx(e->get_id(), r);
+    ctx.push_idx(set_vector_idx_trail(m_translate, e->get_id()));
+}
+
+void bv2int_translator::internalize_bv(app* e) {
+    ensure_translated(e);
+    if (m.is_bool(e)) {
+        m_preds.push_back(e);
+        ctx.push(push_back_vector(m_preds));
+    }
+}
+
+void bv2int_translator::ensure_translated(expr* e) {
+    if (m_translate.get(e->get_id(), nullptr))
+        return;
+    ptr_vector<expr> todo;
+    ast_fast_mark1 visited;
+    todo.push_back(e);
+    visited.mark(e);
+    for (unsigned i = 0; i < todo.size(); ++i) {
+        expr* e = todo[i];
+        if (!is_app(e))
+            continue;
+        app* a = to_app(e);
+        if (m.is_bool(e) && a->get_family_id() != bv.get_family_id())
+            continue;
+        for (auto arg : *a)
+            if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) {
+                visited.mark(arg);
+                todo.push_back(arg);
+            }
+    }
+    std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
+    for (expr* e : todo)
+        translate_expr(e);
+}
+
+rational bv2int_translator::bv_size(expr* bv_expr) {
+    return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort()));
+}
+
+void bv2int_translator::translate_expr(expr* e) {
+    if (is_quantifier(e))
+        translate_quantifier(to_quantifier(e));
+    else if (is_var(e))
+        translate_var(to_var(e));
+    else {
+        app* ap = to_app(e);
+        if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
+            set_translated(e, e);
+            return;
+        }
+        m_args.reset();
+        for (auto arg : *ap)
+            m_args.push_back(translated(arg));
+
+        if (ap->get_family_id() == basic_family_id)
+            translate_basic(ap);
+        else if (ap->get_family_id() == bv.get_family_id())
+            translate_bv(ap);
+        else
+            translate_app(ap);
+    }
+}
+
+void bv2int_translator::translate_quantifier(quantifier* q) {
+    if (m_is_plugin) {
+        set_translated(q, q);
+        return;
+    }
+    if (is_lambda(q))
+        throw default_exception("lambdas are not supported in intblaster");
+    expr* b = q->get_expr();
+    unsigned nd = q->get_num_decls();
+    ptr_vector<sort> sorts;
+    for (unsigned i = 0; i < nd; ++i) {
+        auto s = q->get_decl_sort(i);
+        if (bv.is_bv_sort(s)) {
+            NOT_IMPLEMENTED_YET();
+            sorts.push_back(a.mk_int());
+        }
+        else
+            sorts.push_back(s);
+    }
+    b = translated(b);
+    // TODO if sorts contain integer, then created bounds variables.       
+    set_translated(q, m.update_quantifier(q, b));
+}
+
+void bv2int_translator::translate_var(var* v) {
+    if (bv.is_bv_sort(v->get_sort()))
+        set_translated(v, m.mk_var(v->get_idx(), a.mk_int()));
+    else
+        set_translated(v, v);
+}
+
+// Translate functions that are not built-in or bit-vectors.
+// Base method uses fresh functions.
+// Other method could use bv2int, int2bv axioms and coercions.
+// f(args) = bv2int(f(int2bv(args'))
+//
+
+void bv2int_translator::translate_app(app* e) {
+
+    if (m_is_plugin && m.is_bool(e)) {
+        set_translated(e, e);
+        return;
+    }
+
+    bool has_bv_sort = bv.is_bv(e);
+    func_decl* f = e->get_decl();
+
+    for (unsigned i = 0; i < m_args.size(); ++i)
+        if (bv.is_bv(e->get_arg(i)))
+            m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
+
+    if (has_bv_sort)
+        m_vars.push_back(e);
+    if (m_is_plugin) {
+        expr* r = m.mk_app(f, m_args);
+        if (has_bv_sort) {
+            ctx.push(push_back_vector(m_vars));
+            r = bv.mk_bv2int(r);
+        }
+        set_translated(e, r);
+        return;
+    }
+    else if (has_bv_sort) {
+        if (f->get_family_id() != null_family_id)
+            throw default_exception("conversion for interpreted functions is not supported by intblast solver");
+        func_decl* g = nullptr;
+        if (!m_new_funs.find(f, g)) {
+            g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int());
+            m_new_funs.insert(f, g);
+        }
+        f = g;
+        m_pinned.push_back(f);
+    }
+    set_translated(e, m.mk_app(f, m_args));
+}
+
+void bv2int_translator::translate_bv(app* e) {
+
+    auto bnot = [&](expr* e) {
+        return a.mk_sub(a.mk_int(-1), e);
+        };
+
+    auto band = [&](expr_ref_vector const& args) {
+        expr* r = arg(0);
+        for (unsigned i = 1; i < args.size(); ++i)
+            r = a.mk_band(bv.get_bv_size(e), r, arg(i));
+        return r;
+        };
+
+    auto rotate_left = [&](unsigned n) {
+        auto sz = bv.get_bv_size(e);
+        n = n % sz;
+        expr* r = arg(0);
+        if (n != 0 && sz != 1) {
+            // r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n]
+            // r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)???
+            // r * A + (r div B) mod A
+            auto N = bv_size(e);
+            auto A = rational::power_of_two(sz - n);
+            auto B = rational::power_of_two(n);
+            auto hi = mul(r, a.mk_int(A));
+            auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
+            r = add(hi, lo);
+        }
+        return r;
+        };
+
+    expr* bv_expr = e;
+    expr_ref r(m);
+    auto const& args = m_args;
+    switch (e->get_decl_kind()) {
+    case OP_BADD:
+        r = a.mk_add(args);
+        break;
+    case OP_BSUB:
+        r = a.mk_sub(args.size(), args.data());
+        break;
+    case OP_BMUL:
+        r = a.mk_mul(args);
+        break;
+    case OP_ULEQ:
+        bv_expr = e->get_arg(0);
+        r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
+        break;
+    case OP_UGEQ:
+        bv_expr = e->get_arg(0);
+        r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
+        break;
+    case OP_ULT:
+        bv_expr = e->get_arg(0);
+        r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
+        break;
+    case OP_UGT:
+        bv_expr = e->get_arg(0);
+        r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
+        break;
+    case OP_SLEQ:
+        bv_expr = e->get_arg(0);
+        r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
+        break;
+    case OP_SGEQ:
+        bv_expr = e->get_arg(0);
+        r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
+        break;
+    case OP_SLT:
+        bv_expr = e->get_arg(0);
+        r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
+        break;
+    case OP_SGT:
+        bv_expr = e->get_arg(0);
+        r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
+        break;
+    case OP_BNEG:
+        r = a.mk_uminus(arg(0));
+        break;
+    case OP_CONCAT: {
+        unsigned sz = 0;
+        expr_ref new_arg(m);
+        for (unsigned i = args.size(); i-- > 0;) {
+            expr* old_arg = e->get_arg(i);
+            new_arg = umod(old_arg, i);
+            if (sz > 0) {
+                new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
+                r = add(r, new_arg);
+            }
+            else
+                r = new_arg;
+            sz += bv.get_bv_size(old_arg->get_sort());
+        }
+        break;
+    }
+    case OP_EXTRACT: {
+        unsigned lo, hi;
+        expr* old_arg;
+        VERIFY(bv.is_extract(e, lo, hi, old_arg));
+        r = arg(0);
+        if (lo > 0)
+            r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
+        break;
+    }
+    case OP_BV_NUM: {
+        rational val;
+        unsigned sz;
+        VERIFY(bv.is_numeral(e, val, sz));
+        r = a.mk_int(val);
+        break;
+    }
+    case OP_BUREM:
+    case OP_BUREM_I: {
+        expr* x = umod(e, 0), * y = umod(e, 1);
+        r = if_eq(y, 0, x, a.mk_mod(x, y));
+        break;
+    }
+    case OP_BUDIV:
+    case OP_BUDIV_I: {
+        expr* x = umod(e, 0), * y = umod(e, 1);
+        r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
+        break;
+    }
+    case OP_BUMUL_NO_OVFL: {
+        bv_expr = e->get_arg(0);
+        r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
+        break;
+    }
+    case OP_BSHL: {
+        if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
+            r = a.mk_shl(bv.get_bv_size(e), arg(0), arg(1));
+        else {
+            expr* x = arg(0), * y = umod(e, 1);
+            r = a.mk_int(0);
+            IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
+            for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
+                r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);
+        }
+        break;
+    }
+    case OP_BNOT:
+        r = bnot(arg(0));
+        break;
+    case OP_BLSHR:
+        if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
+            r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
+        else {
+            expr* x = arg(0), * y = umod(e, 1);
+            r = a.mk_int(0);
+            IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
+            for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
+                r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
+        }
+        break;
+    case OP_BASHR:
+        if (!a.is_numeral(arg(1)))
+            r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
+        else {
+
+            //
+            // ashr(x, y)
+            // if y = k & x >= 0 -> x / 2^k   
+            // if y = k & x < 0  -> (x / 2^k) - 2^{N-k}
+            //
+            unsigned sz = bv.get_bv_size(e);
+            rational N = bv_size(e);
+            expr* x = umod(e, 0), * y = umod(e, 1);
+            expr* signx = a.mk_ge(x, a.mk_int(N / 2));
+            r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0));
+            IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
+                r = if_eq(y, i,
+                    m.mk_ite(signx, add(d, a.mk_int(-rational::power_of_two(sz - i))), d),
+                    r);
+            }
+        }
+        break;
+    case OP_BOR:
+        // p | q := (p + q) - band(p, q)
+        IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
+        r = arg(0);
+        for (unsigned i = 1; i < args.size(); ++i)
+            r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
+        break;
+    case OP_BNAND:
+        r = bnot(band(args));
+        break;
+    case OP_BAND:
+        IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
+        r = band(args);
+        break;
+    case OP_BXNOR:
+    case OP_BXOR: {
+        // p ^ q := (p + q) - 2*band(p, q);
+        unsigned sz = bv.get_bv_size(e);
+        IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
+        r = arg(0);
+        for (unsigned i = 1; i < args.size(); ++i) {
+            expr* q = arg(i);
+            r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
+        }
+        if (e->get_decl_kind() == OP_BXNOR)
+            r = bnot(r);
+        break;
+    }
+    case OP_ZERO_EXT:
+        bv_expr = e->get_arg(0);
+        r = umod(bv_expr, 0);
+        SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
+        break;
+    case OP_SIGN_EXT: {
+        bv_expr = e->get_arg(0);
+        r = umod(bv_expr, 0);
+        SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
+        unsigned arg_sz = bv.get_bv_size(bv_expr);
+        //unsigned sz = bv.get_bv_size(e);
+        // rational N = rational::power_of_two(sz);
+        rational M = rational::power_of_two(arg_sz);
+        expr* signbit = a.mk_ge(r, a.mk_int(M / 2));
+        r = m.mk_ite(signbit, a.mk_sub(r, a.mk_int(M)), r);
+        break;
+    }
+    case OP_INT2BV:
+        m_int2bv.push_back(e);
+        ctx.push(push_back_vector(m_int2bv));
+        r = arg(0);
+        break;
+    case OP_BV2INT:
+        m_bv2int.push_back(e);
+        ctx.push(push_back_vector(m_bv2int));
+        r = umod(e->get_arg(0), 0);
+        break;
+    case OP_BCOMP:
+        bv_expr = e->get_arg(0);
+        r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
+        break;
+    case OP_BSMOD_I:
+    case OP_BSMOD: {
+        expr* x = umod(e, 0), * y = umod(e, 1);
+        rational N = bv_size(e);
+        expr* signx = a.mk_ge(x, a.mk_int(N / 2));
+        expr* signy = a.mk_ge(y, a.mk_int(N / 2));
+        expr* u = a.mk_mod(x, y);
+        // u = 0 ->  0
+        // y = 0 ->  x
+        // x < 0, y < 0 ->  -u
+        // x < 0, y >= 0 ->  y - u
+        // x >= 0, y < 0 ->  y + u
+        // x >= 0, y >= 0 ->  u
+        r = a.mk_uminus(u);
+        r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
+        r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
+        r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
+        r = if_eq(u, 0, a.mk_int(0), r);
+        r = if_eq(y, 0, x, r);
+        break;
+    }
+    case OP_BSDIV_I:
+    case OP_BSDIV: {
+        // d = udiv(abs(x), abs(y))
+        // y = 0, x > 0 -> 1
+        // y = 0, x <= 0 -> -1
+        // x = 0, y != 0 -> 0
+        // x > 0, y < 0 -> -d
+        // x < 0, y > 0 -> -d
+        // x > 0, y > 0 -> d
+        // x < 0, y < 0 -> d
+        expr* x = umod(e, 0), * y = umod(e, 1);
+        rational N = bv_size(e);
+        expr* signx = a.mk_ge(x, a.mk_int(N / 2));
+        expr* signy = a.mk_ge(y, a.mk_int(N / 2));
+        x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
+        y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
+        expr* d = a.mk_idiv(x, y);
+        r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
+        r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
+        break;
+    }
+    case OP_BSREM_I:
+    case OP_BSREM: {
+        // y = 0 -> x
+        // else x - sdiv(x, y) * y
+        expr* x = umod(e, 0), * y = umod(e, 1);
+        rational N = bv_size(e);
+        expr* signx = a.mk_ge(x, a.mk_int(N / 2));
+        expr* signy = a.mk_ge(y, a.mk_int(N / 2));
+        expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
+        expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
+        expr* d = a.mk_idiv(absx, absy);
+        d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
+        r = a.mk_sub(x, mul(d, y));
+        r = if_eq(y, 0, x, r);
+        break;
+    }
+    case OP_ROTATE_LEFT: {
+        auto n = e->get_parameter(0).get_int();
+        r = rotate_left(n);
+        break;
+    }
+    case OP_ROTATE_RIGHT: {
+        unsigned sz = bv.get_bv_size(e);
+        auto n = e->get_parameter(0).get_int();
+        r = rotate_left(sz - n);
+        break;
+    }
+    case OP_EXT_ROTATE_LEFT: {
+        unsigned sz = bv.get_bv_size(e);
+        expr* y = umod(e, 1);
+        r = a.mk_int(0);
+        for (unsigned i = 0; i < sz; ++i)
+            r = if_eq(y, i, rotate_left(i), r);
+        break;
+    }
+    case OP_EXT_ROTATE_RIGHT: {
+        unsigned sz = bv.get_bv_size(e);
+        expr* y = umod(e, 1);
+        r = a.mk_int(0);
+        for (unsigned i = 0; i < sz; ++i)
+            r = if_eq(y, i, rotate_left(sz - i), r);
+        break;
+    }
+    case OP_REPEAT: {
+        unsigned n = e->get_parameter(0).get_int();
+        expr* x = umod(e->get_arg(0), 0);
+        r = x;
+        rational N = bv_size(e->get_arg(0));
+        rational N0 = N;
+        for (unsigned i = 1; i < n; ++i)
+            r = add(mul(a.mk_int(N), x), r), N *= N0;
+        break;
+    }
+    case OP_BREDOR: {
+        r = umod(e->get_arg(0), 0);
+        r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
+        break;
+    }
+    case OP_BREDAND: {
+        rational N = bv_size(e->get_arg(0));
+        r = umod(e->get_arg(0), 0);
+        r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1)));
+        break;
+    }
+    default:
+        verbose_stream() << mk_pp(e, m) << "\n";
+        NOT_IMPLEMENTED_YET();
+    }
+    set_translated(e, r);
+}
+
+expr_ref bv2int_translator::if_eq(expr* n, unsigned k, expr* th, expr* el) {
+    rational r;
+    expr_ref _th(th, m), _el(el, m);
+    if (bv.is_numeral(n, r)) {
+        if (r == k)
+            return expr_ref(th, m);
+        else
+            return expr_ref(el, m);
+    }
+    return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m);
+}
+
+void bv2int_translator::translate_basic(app* e) {
+    if (m.is_eq(e)) {
+        bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
+        if (has_bv_arg) {
+            expr* bv_expr = e->get_arg(0);
+            rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
+            if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) ||
+                is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
+                set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
+            }
+            else {
+                m_args[0] = a.mk_sub(arg(0), arg(1));
+                set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
+            }
+        }
+        else
+            set_translated(e, m.mk_eq(arg(0), arg(1)));
+    }
+    else if (m.is_ite(e))
+        set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
+    else if (m_is_plugin)
+        set_translated(e, e);
+    else
+        set_translated(e, m.mk_app(e->get_decl(), m_args));
+}
+
+bool bv2int_translator::is_bounded(expr* x, rational const& N) {
+    return any_of(m_vars, [&](expr* v) {
+        return is_translated(v) && translated(v) == x && bv_size(v) <= N;
+        });
+}
+
+bool bv2int_translator::is_non_negative(expr* bv_expr, expr* e) {
+    auto N = rational::power_of_two(bv.get_bv_size(bv_expr));
+    rational r;
+    if (a.is_numeral(e, r))
+        return r >= 0;
+    if (is_bounded(e, N))
+        return true;
+    expr* x = nullptr, * y = nullptr;
+    if (a.is_mul(e, x, y))
+        return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
+    if (a.is_add(e, x, y))
+        return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
+    return false;
+}
+
+expr* bv2int_translator::umod(expr* bv_expr, unsigned i) {
+    expr* x = arg(i);
+    rational N = bv_size(bv_expr);
+    return amod(bv_expr, x, N);
+}
+
+expr* bv2int_translator::smod(expr* bv_expr, unsigned i) {
+    expr* x = arg(i);
+    auto N = bv_size(bv_expr);
+    auto shift = N / 2;
+    rational r;
+    if (a.is_numeral(x, r))
+        return a.mk_int(mod(r + shift, N));
+    return amod(bv_expr, add(x, a.mk_int(shift)), N);
+}
+
+expr_ref bv2int_translator::mul(expr* x, expr* y) {
+    expr_ref _x(x, m), _y(y, m);
+    if (a.is_zero(x))
+        return _x;
+    if (a.is_zero(y))
+        return _y;
+    if (a.is_one(x))
+        return _y;
+    if (a.is_one(y))
+        return _x;
+    rational v1, v2;
+    if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
+        return expr_ref(a.mk_int(v1 * v2), m);
+    _x = a.mk_mul(x, y);
+    return _x;
+}
+
+expr_ref bv2int_translator::add(expr* x, expr* y) {
+    expr_ref _x(x, m), _y(y, m);
+    if (a.is_zero(x))
+        return _y;
+    if (a.is_zero(y))
+        return _x;
+    rational v1, v2;
+    if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
+        return expr_ref(a.mk_int(v1 + v2), m);
+    _x = a.mk_add(x, y);
+    return _x;
+}
+
+/*
+* Perform simplifications that are claimed sound when the bit-vector interpretations of
+* mod/div always guard the mod and dividend to be non-zero.
+* Potentially shady area is for arithmetic expressions created by int2bv.
+* They will be guarded by a modulus which does not disappear.
+*/
+expr* bv2int_translator::amod(expr* bv_expr, expr* x, rational const& N) {
+    rational v;
+    expr* r = nullptr, * c = nullptr, * t = nullptr, * e = nullptr;
+    if (m.is_ite(x, c, t, e))
+        r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
+    else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
+        r = x;
+    else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
+        r = x;
+    else if (a.is_numeral(x, v))
+        r = a.mk_int(mod(v, N));
+    else if (is_bounded(x, N))
+        r = x;
+    else
+        r = a.mk_mod(x, a.mk_int(N));
+    return r;
+}
+
+void bv2int_translator::translate_eq(expr* e) {
+    expr* x = nullptr, * y = nullptr;
+    VERIFY(m.is_eq(e, x, y));
+    SASSERT(bv.is_bv(x));
+    if (!is_translated(e)) {
+        ensure_translated(x);
+        ensure_translated(y);
+        m_args.reset();
+        m_args.push_back(a.mk_sub(translated(x), translated(y)));
+        set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
+    }
+    m_preds.push_back(e);
+    TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");
+    ctx.push(push_back_vector(m_preds));
+
+}
diff --git a/src/ast/rewriter/bv2int_translator.h b/src/ast/rewriter/bv2int_translator.h
new file mode 100644
index 000000000..c84b86f56
--- /dev/null
+++ b/src/ast/rewriter/bv2int_translator.h
@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    bv2int_translator
+    Utilities for translating bit-vector constraints into arithmetic.
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-27
+
+
+--*/
+#pragma once
+
+#include "util/trail.h"
+
+class bv2int_translator_trail {
+public:
+    virtual void push(push_back_vector<expr_ref_vector> const& c) = 0;
+    virtual void push(push_back_vector<ptr_vector<app>> const& c) = 0;
+    virtual void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) = 0;
+};
+
+class bv2int_translator {
+    ast_manager& m;
+    bv2int_translator_trail& ctx;
+    bv_util bv;
+    arith_util a;
+    obj_map<func_decl, func_decl*> m_new_funs;
+    expr_ref_vector m_translate, m_args;
+    ast_ref_vector m_pinned;
+    ptr_vector<app> m_bv2int, m_int2bv;
+    expr_ref_vector m_vars, m_preds;
+    bool m_is_plugin = true;
+
+    void set_translated(expr* e, expr* r);
+    expr* arg(unsigned i) { return m_args.get(i); }
+    
+    expr* umod(expr* bv_expr, unsigned i);
+    expr* smod(expr* bv_expr, unsigned i);
+    bool is_bounded(expr* v, rational const& N);
+    bool is_non_negative(expr* bv_expr, expr* e);
+    expr_ref mul(expr* x, expr* y);
+    expr_ref add(expr* x, expr* y);
+    expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
+    expr* amod(expr* bv_expr, expr* x, rational const& N);
+    rational bv_size(expr* bv_expr);
+    
+    void translate_bv(app* e);
+    void translate_basic(app* e);
+    void translate_app(app* e);
+    void translate_quantifier(quantifier* q);
+    void translate_var(var* v);
+    
+
+public:
+    bv2int_translator(ast_manager& m, bv2int_translator_trail& ctx);
+
+    void ensure_translated(expr* e);
+
+    void translate_eq(expr* e);
+
+    bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
+    expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
+
+    void internalize_bv(app* e);
+    void translate_expr(expr* e);
+
+    expr_ref_vector const& vars() const { return m_vars; }
+    expr_ref_vector const& preds() const { return m_preds; }
+    ptr_vector<app> const& bv2int() const { return m_bv2int; }
+    ptr_vector<app> const& int2bv() const { return m_int2bv; }
+
+    void reset(bool is_plugin);
+       
+};
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index d6dfe57d7..cef918a95 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -22,6 +22,10 @@ Author:
 
 namespace intblast {
 
+    void translator_trail::push(push_back_vector<expr_ref_vector> const& c) { ctx.push(c); }
+    void translator_trail::push(push_back_vector<ptr_vector<app>> const& c) { ctx.push(c); }
+    void translator_trail::push_idx(set_vector_idx_trail<expr_ref_vector> const& c) { ctx.push(c); }
+
     solver::solver(euf::solver& ctx) :
         th_euf_solver(ctx, symbol("intblast"), ctx.get_manager().get_family_id("bv")),
         ctx(ctx),
@@ -29,9 +33,8 @@ namespace intblast {
         m(ctx.get_manager()),
         bv(m),
         a(m),
-        m_translate(m),
-        m_args(m),
-        m_pinned(m)
+        trail(ctx),
+        m_translator(m, trail)
     {}
 
     euf::theory_var solver::mk_var(euf::enode* n) {
@@ -85,49 +88,22 @@ namespace intblast {
         SASSERT(!n->is_attached_to(get_id()));
         mk_var(n);
         SASSERT(n->is_attached_to(get_id()));
-        internalize_bv(a);
+        m_translator.internalize_bv(a);
         return true;
     }
 
     void solver::eq_internalized(euf::enode* n) {
-        expr* e = n->get_expr();
-        expr* x = nullptr, * y = nullptr;
-        VERIFY(m.is_eq(n->get_expr(), x, y));
-        SASSERT(bv.is_bv(x));
-        if (!is_translated(e)) {
-            ensure_translated(x);
-            ensure_translated(y);
-            m_args.reset();
-            m_args.push_back(a.mk_sub(translated(x), translated(y)));
-            set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
-        }
-        m_preds.push_back(e);
-        TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");
-        ctx.push(push_back_vector(m_preds));
-    }
-
-    void solver::set_translated(expr* e, expr* r) { 
-        SASSERT(r);
-        SASSERT(!is_translated(e));          
-        m_translate.setx(e->get_id(), r); 
-        ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
-    }
-
-    void solver::internalize_bv(app* e) {
-        ensure_translated(e);
-        if (m.is_bool(e)) {
-            m_preds.push_back(e);
-            ctx.push(push_back_vector(m_preds));
-        }
+        m_translator.translate_eq(n->get_expr());
     }
 
     bool solver::add_bound_axioms() {
-        if (m_vars_qhead == m_vars.size())
+        auto const& vars = m_translator.vars();
+        if (m_vars_qhead == vars.size())
             return false;
         ctx.push(value_trail(m_vars_qhead));
-        for (; m_vars_qhead < m_vars.size(); ++m_vars_qhead) {
-            auto v = m_vars[m_vars_qhead];
-            auto w = translated(v);
+        for (; m_vars_qhead < vars.size(); ++m_vars_qhead) {
+            auto v = vars[m_vars_qhead];
+            auto w = m_translator.translated(v);
             auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort()));
             auto lo = ctx.mk_literal(a.mk_ge(w, a.mk_int(0)));
             auto hi = ctx.mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
@@ -140,12 +116,13 @@ namespace intblast {
     }
 
     bool solver::add_predicate_axioms() {
-        if (m_preds_qhead == m_preds.size())
+        auto const& preds = m_translator.preds();
+        if (m_preds_qhead == preds.size())
             return false;
         ctx.push(value_trail(m_preds_qhead));
-        for (; m_preds_qhead < m_preds.size(); ++m_preds_qhead) {
-            expr* e = m_preds[m_preds_qhead];
-            expr_ref r(translated(e), m);
+        for (; m_preds_qhead < preds.size(); ++m_preds_qhead) {
+            expr* e = preds[m_preds_qhead];
+            expr_ref r(m_translator.translated(e), m);
             ctx.get_rewriter()(r);
             auto a = expr2literal(e);
             auto b = mk_literal(r);
@@ -158,31 +135,7 @@ namespace intblast {
 
     bool solver::unit_propagate() {
         return add_bound_axioms() || add_predicate_axioms();
-    }
-    void solver::ensure_translated(expr* e) {
-        if (m_translate.get(e->get_id(), nullptr))
-            return;
-        ptr_vector<expr> todo;
-        ast_fast_mark1 visited;
-        todo.push_back(e);
-        visited.mark(e);
-        for (unsigned i = 0; i < todo.size(); ++i) {
-            expr* e = todo[i];
-            if (!is_app(e))
-                continue;
-            app* a = to_app(e);
-            if (m.is_bool(e) && a->get_family_id() != bv.get_family_id())
-                continue;
-            for (auto arg : *a)
-                if (!visited.is_marked(arg) && !m_translate.get(arg->get_id(), nullptr)) {
-                    visited.mark(arg);
-                    todo.push_back(arg);
-                }
-        }
-        std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
-        for (expr* e : todo)            
-            translate_expr(e);
-    }
+    }    
 
     lbool solver::check_axiom(sat::literal_vector const& lits) {
         sat::literal_vector core;
@@ -198,14 +151,10 @@ namespace intblast {
     }
 
     lbool solver::check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
-        m_core.reset();
-        m_vars.reset();
         m_is_plugin = false;
+        m_translator.reset(false);
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
-        for (unsigned i = 0; i < m_translate.size(); ++i)
-            m_translate[i] = nullptr;
-
         expr_ref_vector es(m), original_es(m);
         for (auto lit : lits)
             es.push_back(ctx.literal2expr(lit));
@@ -222,8 +171,8 @@ namespace intblast {
         
             translate(es);
             
-            for (auto e : m_vars) {
-                auto v = translated(e);
+            for (auto e : m_translator.vars()) {
+                auto v = m_translator.translated(e);
                 auto b = rational::power_of_two(bv.get_bv_size(e));
                 m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
                 m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
@@ -331,8 +280,8 @@ namespace intblast {
 
         translate(es);
 
-        for (auto e : m_vars) {
-            auto v = translated(e);
+        for (auto e : m_translator.vars()) {
+            auto v = m_translator.translated(e);
             auto b = rational::power_of_two(bv.get_bv_size(e));
             m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
             m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
@@ -377,7 +326,7 @@ namespace intblast {
     void solver::sorted_subterms(expr_ref_vector& es, ptr_vector<expr>& sorted) {
         expr_fast_mark1 visited;
         for (expr* e : es) {
-            if (is_translated(e))
+            if (m_translator.is_translated(e))
                 continue;
             if (visited.is_marked(e))
                 continue;
@@ -389,7 +338,7 @@ namespace intblast {
             if (is_app(e)) {
                 app* a = to_app(e);
                 for (expr* arg : *a) {
-                    if (!visited.is_marked(arg) && !is_translated(arg)) {
+                    if (!visited.is_marked(arg) && !m_translator.is_translated(arg)) {
                         visited.mark(arg);
                         sorted.push_back(arg);
                     }
@@ -399,7 +348,7 @@ namespace intblast {
             else if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
                 expr* b = q->get_expr();
-                if (!visited.is_marked(b) && !is_translated(b)) {
+                if (!visited.is_marked(b) && !m_translator.is_translated(b)) {
                     visited.mark(b);
                     sorted.push_back(b);
                 }
@@ -414,20 +363,20 @@ namespace intblast {
         sorted_subterms(es, todo);
 
         for (expr* e : todo)
-            translate_expr(e);
+            m_translator.translate_expr(e);
 
         TRACE("bv",
             for (expr* e : es)
-                tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n";
+                tout << mk_pp(e, m) << "\n->\n" << mk_pp(m_translator.translated(e), m) << "\n";
         );
 
         for (unsigned i = 0; i < es.size(); ++i)
-            es[i] = translated(es.get(i));
+            es[i] = m_translator.translated(es.get(i));
     }
 
     sat::check_result solver::check() { 
         // ensure that bv2int is injective
-        for (auto e : m_bv2int) {
+        for (auto e : m_translator.bv2int()) {
             euf::enode* n = expr2enode(e);
             euf::enode* r1 = n->get_arg(0)->get_root();
             for (auto sib : euf::enode_class(n)) {
@@ -449,7 +398,7 @@ namespace intblast {
         }
         // ensure that int2bv respects values
         // bv2int(int2bv(x)) = x mod N
-        for (auto e : m_int2bv) {
+        for (auto e : m_translator.int2bv()) {
             auto n = expr2enode(e);
             auto x = n->get_arg(0)->get_expr();
             auto bv2int = bv.mk_bv2int(e);
@@ -469,595 +418,12 @@ namespace intblast {
         return sat::check_result::CR_DONE; 
     }
 
-    bool solver::is_bounded(expr* x, rational const& N) {
-        return any_of(m_vars, [&](expr* v) {
-            return is_translated(v) && translated(v) == x && bv_size(v) <= N;
-        });
-    }
-
-    bool solver::is_non_negative(expr* bv_expr, expr* e) {
-        auto N = rational::power_of_two(bv.get_bv_size(bv_expr));
-        rational r;
-        if (a.is_numeral(e, r))
-            return r >= 0;
-        if (is_bounded(e, N))
-            return true;
-        expr* x = nullptr, * y = nullptr;
-        if (a.is_mul(e, x, y)) 
-            return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
-        if (a.is_add(e, x, y))
-            return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
-        return false;
-    }
-
-    expr* solver::umod(expr* bv_expr, unsigned i) {
-        expr* x = arg(i);
-        rational N = bv_size(bv_expr);
-        return amod(bv_expr, x, N);
-    }
-
-    expr* solver::smod(expr* bv_expr, unsigned i) {
-        expr* x = arg(i);
-        auto N = bv_size(bv_expr);
-        auto shift = N / 2;
-        rational r;
-        if (a.is_numeral(x, r))
-            return a.mk_int(mod(r + shift, N));
-        return amod(bv_expr, add(x, a.mk_int(shift)), N);
-    }
-
-    expr_ref solver::mul(expr* x, expr* y) {
-        expr_ref _x(x, m), _y(y, m);
-        if (a.is_zero(x))
-            return _x;
-        if (a.is_zero(y))
-            return _y;
-        if (a.is_one(x))
-            return _y;
-        if (a.is_one(y))
-            return _x;
-        rational v1, v2;
-        if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
-            return expr_ref(a.mk_int(v1 * v2), m);
-        _x = a.mk_mul(x, y);
-        return _x;
-    }
-
-    expr_ref solver::add(expr* x, expr* y) {
-        expr_ref _x(x, m), _y(y, m);
-        if (a.is_zero(x))
-            return _y;
-        if (a.is_zero(y))
-            return _x;
-        rational v1, v2;
-        if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
-            return expr_ref(a.mk_int(v1 + v2), m);
-        _x = a.mk_add(x, y);
-        return _x;
-    }
-
-    /*
-    * Perform simplifications that are claimed sound when the bit-vector interpretations of
-    * mod/div always guard the mod and dividend to be non-zero.
-    * Potentially shady area is for arithmetic expressions created by int2bv. 
-    * They will be guarded by a modulus which does not disappear.
-    */
-    expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
-        rational v;
-        expr* r = nullptr, *c = nullptr, * t = nullptr, * e = nullptr;
-        if (m.is_ite(x, c, t, e))
-            r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
-        else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
-            r = x;
-        else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
-            r = x;
-        else if (a.is_numeral(x, v))
-            r = a.mk_int(mod(v, N));
-        else if (is_bounded(x, N))
-            r = x;
-        else 
-            r = a.mk_mod(x, a.mk_int(N));
-        return r;
-    }
-
-    rational solver::bv_size(expr* bv_expr) {
-        return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort()));
-    }
-
-    void solver::translate_expr(expr* e) {
-        if (is_quantifier(e))
-            translate_quantifier(to_quantifier(e));
-        else if (is_var(e))
-            translate_var(to_var(e));
-        else {
-            app* ap = to_app(e);
-            if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
-                set_translated(e, e);
-                return;
-            }
-            m_args.reset();
-            for (auto arg : *ap)
-                m_args.push_back(translated(arg));
-
-            if (ap->get_family_id() == basic_family_id)
-                translate_basic(ap);
-            else if (ap->get_family_id() == bv.get_family_id())
-                translate_bv(ap);
-            else
-                translate_app(ap);
-        }
-    }
-
-    void solver::translate_quantifier(quantifier* q) {
-        if (m_is_plugin) {
-            set_translated(q, q);
-            return;
-        }
-        if (is_lambda(q))
-            throw default_exception("lambdas are not supported in intblaster");
-        expr* b = q->get_expr();
-        unsigned nd = q->get_num_decls();
-        ptr_vector<sort> sorts;
-        for (unsigned i = 0; i < nd; ++i) {
-            auto s = q->get_decl_sort(i);
-            if (bv.is_bv_sort(s)) {
-                NOT_IMPLEMENTED_YET();
-                sorts.push_back(a.mk_int());
-            }
-            else
-                sorts.push_back(s);
-        }
-        b = translated(b);
-        // TODO if sorts contain integer, then created bounds variables.       
-        set_translated(q, m.update_quantifier(q, b));
-    }
-
-    void solver::translate_var(var* v) {
-        if (bv.is_bv_sort(v->get_sort()))
-            set_translated(v, m.mk_var(v->get_idx(), a.mk_int()));
-        else
-            set_translated(v, v);
-    }
-
-    // Translate functions that are not built-in or bit-vectors.
-    // Base method uses fresh functions.
-    // Other method could use bv2int, int2bv axioms and coercions.
-    // f(args) = bv2int(f(int2bv(args'))
-    //
-
-    void solver::translate_app(app* e) {
-
-        if (m_is_plugin && m.is_bool(e)) {
-            set_translated(e, e);
-            return;
-        }
-
-        bool has_bv_sort = bv.is_bv(e);
-        func_decl* f = e->get_decl();
-
-        for (unsigned i = 0; i < m_args.size(); ++i)
-            if (bv.is_bv(e->get_arg(i)))
-                m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
-
-        if (has_bv_sort)
-            m_vars.push_back(e);        
-        if (m_is_plugin) {
-            expr* r = m.mk_app(f, m_args);
-            if (has_bv_sort) {
-                ctx.push(push_back_vector(m_vars));
-                r = bv.mk_bv2int(r);
-            }
-            set_translated(e, r);
-            return;
-        }
-        else if (has_bv_sort) {
-            if (f->get_family_id() != null_family_id)
-                throw default_exception("conversion for interpreted functions is not supported by intblast solver");
-            func_decl* g = nullptr;
-            if (!m_new_funs.find(f, g)) {
-                g = m.mk_fresh_func_decl(e->get_decl()->get_name(), symbol("bv"), f->get_arity(), f->get_domain(), a.mk_int());
-                m_new_funs.insert(f, g);
-            }
-            f = g;
-            m_pinned.push_back(f);
-        }
-        set_translated(e, m.mk_app(f, m_args));        
-    }
-
-    void solver::translate_bv(app* e) {
-
-        auto bnot = [&](expr* e) {
-            return a.mk_sub(a.mk_int(-1), e);
-            };
-
-        auto band = [&](expr_ref_vector const& args) {
-            expr* r = arg(0);
-            for (unsigned i = 1; i < args.size(); ++i)
-                r = a.mk_band(bv.get_bv_size(e), r, arg(i));
-            return r;
-            };
-
-        auto rotate_left = [&](unsigned n) {
-            auto sz = bv.get_bv_size(e);
-            n = n % sz;
-            expr* r = arg(0);
-            if (n != 0 && sz != 1) {
-                // r[sz - n - 1 : 0] ++ r[sz - 1 : sz - n]
-                // r * 2^(sz - n) + (r div 2^n) mod 2^(sz - n)???
-                // r * A + (r div B) mod A
-                auto N = bv_size(e);
-                auto A = rational::power_of_two(sz - n);
-                auto B = rational::power_of_two(n);
-                auto hi = mul(r, a.mk_int(A));
-                auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
-                r = add(hi, lo);
-            }
-            return r;
-        };
-
-        expr* bv_expr = e;
-        expr_ref r(m);
-        auto const& args = m_args;
-        switch (e->get_decl_kind()) {
-        case OP_BADD:
-            r = a.mk_add(args);
-            break;
-        case OP_BSUB:
-            r = a.mk_sub(args.size(), args.data());
-            break;
-        case OP_BMUL:
-            r = a.mk_mul(args);
-            break;
-        case OP_ULEQ:
-            bv_expr = e->get_arg(0);
-            r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
-            break;
-        case OP_UGEQ:
-            bv_expr = e->get_arg(0);
-            r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
-            break;
-        case OP_ULT:
-            bv_expr = e->get_arg(0);
-            r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
-            break;
-        case OP_UGT:
-            bv_expr = e->get_arg(0);
-            r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
-            break;
-        case OP_SLEQ:
-            bv_expr = e->get_arg(0);
-            r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
-            break;
-        case OP_SGEQ:
-            bv_expr = e->get_arg(0);
-            r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
-            break;
-        case OP_SLT:
-            bv_expr = e->get_arg(0);
-            r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
-            break;
-        case OP_SGT:
-            bv_expr = e->get_arg(0);
-            r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
-            break;
-        case OP_BNEG:
-            r = a.mk_uminus(arg(0));
-            break;
-        case OP_CONCAT: {
-            unsigned sz = 0;
-            expr_ref new_arg(m);
-            for (unsigned i = args.size(); i-- > 0;) {
-                expr* old_arg = e->get_arg(i);
-                new_arg = umod(old_arg, i);
-                if (sz > 0) {
-                    new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
-                    r = add(r, new_arg);
-                }
-                else
-                    r = new_arg;
-                sz += bv.get_bv_size(old_arg->get_sort());
-            }
-            break;
-        }
-        case OP_EXTRACT: {
-            unsigned lo, hi;
-            expr* old_arg;
-            VERIFY(bv.is_extract(e, lo, hi, old_arg));
-            r = arg(0);
-            if (lo > 0)
-                r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
-            break;
-        }
-        case OP_BV_NUM: {
-            rational val;
-            unsigned sz;
-            VERIFY(bv.is_numeral(e, val, sz));
-            r = a.mk_int(val);
-            break;
-        }
-        case OP_BUREM:
-        case OP_BUREM_I: {
-            expr* x = umod(e, 0), * y = umod(e, 1);
-            r = if_eq(y, 0, x, a.mk_mod(x, y));
-            break;
-        }
-        case OP_BUDIV:
-        case OP_BUDIV_I: {
-            expr* x = umod(e, 0), * y = umod(e, 1);
-            r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
-            break;
-        }
-        case OP_BUMUL_NO_OVFL: {
-            bv_expr = e->get_arg(0);
-            r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
-            break;
-        }
-        case OP_BSHL: {
-            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) 
-                r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1));
-            else {
-                expr* x = arg(0), * y = umod(e, 1);
-                r = a.mk_int(0);
-                IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
-                for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
-                    r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);   
-            }
-            break;
-        }
-        case OP_BNOT:
-            r = bnot(arg(0));
-            break;
-        case OP_BLSHR: 
-            if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))  
-                r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
-            else {
-                expr* x = arg(0), * y = umod(e, 1);
-                r = a.mk_int(0);
-                IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
-                for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
-                    r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
-            }
-            break;
-        case OP_BASHR: 
-            if (!a.is_numeral(arg(1)))
-                r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
-            else {
-                
-                //
-                // ashr(x, y)
-                // if y = k & x >= 0 -> x / 2^k   
-                // if y = k & x < 0  -> (x / 2^k) - 2^{N-k}
-                //
-                unsigned sz = bv.get_bv_size(e);
-                rational N = bv_size(e);
-                expr* x = umod(e, 0), *y = umod(e, 1);
-                expr* signx = a.mk_ge(x, a.mk_int(N / 2));
-                r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0));
-                IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
-                for (unsigned i = 0; i < sz; ++i) {
-                    expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));              
-                    r = if_eq(y, i,
-                                 m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
-                                 r);
-                }
-            }
-            break;
-        case OP_BOR: 
-            // p | q := (p + q) - band(p, q)
-            IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
-            r = arg(0);
-            for (unsigned i = 1; i < args.size(); ++i)
-                r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
-            break;        
-        case OP_BNAND:
-            r = bnot(band(args));
-            break;
-        case OP_BAND:
-            IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
-            r = band(args);
-            break;
-        case OP_BXNOR:
-        case OP_BXOR: {
-            // p ^ q := (p + q) - 2*band(p, q);
-            unsigned sz = bv.get_bv_size(e);
-            IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
-            r = arg(0);
-            for (unsigned i = 1; i < args.size(); ++i) {
-                expr* q = arg(i);
-                r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
-            }
-            if (e->get_decl_kind() == OP_BXNOR)
-                r = bnot(r);
-            break;
-        }
-        case OP_ZERO_EXT:
-            bv_expr = e->get_arg(0);
-            r = umod(bv_expr, 0);
-            SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
-            break;
-        case OP_SIGN_EXT: {
-            bv_expr = e->get_arg(0);
-            r = umod(bv_expr, 0);
-            SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
-            unsigned arg_sz = bv.get_bv_size(bv_expr);
-            //unsigned sz = bv.get_bv_size(e);
-            // rational N = rational::power_of_two(sz);
-            rational M = rational::power_of_two(arg_sz);
-            expr* signbit = a.mk_ge(r, a.mk_int(M / 2));
-            r = m.mk_ite(signbit, a.mk_sub(r, a.mk_int(M)), r);
-            break;
-        }
-        case OP_INT2BV:
-            m_int2bv.push_back(e);
-            ctx.push(push_back_vector(m_int2bv));
-            r = arg(0);
-            break;
-        case OP_BV2INT:
-            m_bv2int.push_back(e);
-            ctx.push(push_back_vector(m_bv2int));
-            r = umod(e->get_arg(0), 0);
-            break;
-        case OP_BCOMP:
-            bv_expr = e->get_arg(0);
-            r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
-            break;
-        case OP_BSMOD_I:
-        case OP_BSMOD: {            
-            expr* x = umod(e, 0), *y = umod(e, 1);
-            rational N = bv_size(e); 
-            expr* signx = a.mk_ge(x, a.mk_int(N/2));
-            expr* signy = a.mk_ge(y, a.mk_int(N/2));
-            expr* u = a.mk_mod(x, y);
-            // u = 0 ->  0
-            // y = 0 ->  x
-            // x < 0, y < 0 ->  -u
-            // x < 0, y >= 0 ->  y - u
-            // x >= 0, y < 0 ->  y + u
-            // x >= 0, y >= 0 ->  u
-            r = a.mk_uminus(u);   
-            r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
-            r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
-            r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
-            r = if_eq(u, 0, a.mk_int(0), r);
-            r = if_eq(y, 0, x, r);
-            break;
-        } 
-        case OP_BSDIV_I:
-        case OP_BSDIV: {
-            // d = udiv(abs(x), abs(y))
-            // y = 0, x > 0 -> 1
-            // y = 0, x <= 0 -> -1
-            // x = 0, y != 0 -> 0
-            // x > 0, y < 0 -> -d
-            // x < 0, y > 0 -> -d
-            // x > 0, y > 0 -> d
-            // x < 0, y < 0 -> d
-            expr* x = umod(e, 0), * y = umod(e, 1);
-            rational N = bv_size(e);
-            expr* signx = a.mk_ge(x, a.mk_int(N / 2));
-            expr* signy = a.mk_ge(y, a.mk_int(N / 2));
-            x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
-            y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
-            expr* d = a.mk_idiv(x, y);
-            r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
-            r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
-            break;
-        }
-        case OP_BSREM_I:
-        case OP_BSREM: {
-            // y = 0 -> x
-            // else x - sdiv(x, y) * y
-            expr* x = umod(e, 0), * y = umod(e, 1);
-            rational N = bv_size(e);
-            expr* signx = a.mk_ge(x, a.mk_int(N / 2));
-            expr* signy = a.mk_ge(y, a.mk_int(N / 2));
-            expr* absx = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x);
-            expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
-            expr* d = a.mk_idiv(absx, absy);
-            d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
-            r = a.mk_sub(x, mul(d, y));
-            r = if_eq(y, 0, x, r);
-            break;  
-        }
-        case OP_ROTATE_LEFT: {
-            auto n = e->get_parameter(0).get_int();
-            r = rotate_left(n);
-            break;
-        }
-        case OP_ROTATE_RIGHT: {
-            unsigned sz = bv.get_bv_size(e);
-            auto n = e->get_parameter(0).get_int();
-            r = rotate_left(sz - n);
-            break;
-        }
-        case OP_EXT_ROTATE_LEFT:  {
-            unsigned sz = bv.get_bv_size(e);
-            expr* y = umod(e, 1);
-            r = a.mk_int(0);
-            for (unsigned i = 0; i < sz; ++i) 
-                r = if_eq(y, i, rotate_left(i), r);
-            break;
-        }
-        case OP_EXT_ROTATE_RIGHT: {
-            unsigned sz = bv.get_bv_size(e);
-            expr* y = umod(e, 1);
-            r = a.mk_int(0);
-            for (unsigned i = 0; i < sz; ++i) 
-                r = if_eq(y, i, rotate_left(sz - i), r);
-            break;
-        }
-        case OP_REPEAT: {
-            unsigned n = e->get_parameter(0).get_int();
-            expr* x = umod(e->get_arg(0), 0);
-            r = x;
-            rational N = bv_size(e->get_arg(0));
-            rational N0 = N;
-            for (unsigned i = 1; i < n; ++i)
-                r = add(mul(a.mk_int(N), x), r), N *= N0;
-            break;
-        }            
-        case OP_BREDOR: {
-            r = umod(e->get_arg(0), 0);
-            r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
-            break;
-        }
-        case OP_BREDAND: {
-            rational N = bv_size(e->get_arg(0));
-            r = umod(e->get_arg(0), 0);
-            r = m.mk_not(m.mk_eq(r, a.mk_int(N - 1)));
-            break;
-        }
-        default:
-            verbose_stream() << mk_pp(e, m) << "\n";
-            NOT_IMPLEMENTED_YET();
-        }
-        set_translated(e, r);
-    }
-
-    expr_ref solver::if_eq(expr* n, unsigned k, expr* th, expr* el) {
-        rational r;
-        expr_ref _th(th, m), _el(el, m);
-        if (bv.is_numeral(n, r)) {
-            if (r == k)
-                return expr_ref(th, m);
-            else
-                return expr_ref(el, m);
-        }
-        return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m);
-    }
-
-    void solver::translate_basic(app* e) {
-        if (m.is_eq(e)) {
-            bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
-            if (has_bv_arg) {
-                expr* bv_expr = e->get_arg(0);
-                rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
-                if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) || 
-                    is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
-                    set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
-                }
-                else {
-                    m_args[0] = a.mk_sub(arg(0), arg(1));
-                    set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
-                }
-            }
-            else
-                set_translated(e, m.mk_eq(arg(0), arg(1)));
-        }
-        else if (m.is_ite(e))
-            set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
-        else if (m_is_plugin)
-            set_translated(e, e);
-        else 
-            set_translated(e, m.mk_app(e->get_decl(), m_args));        
-    }
-
     rational solver::get_value(expr* e) const {
         SASSERT(bv.is_bv(e));
         model_ref mdl;
         m_solver->get_model(mdl);
         expr_ref r(m);
-        r = translated(e);
+        r = m_translator.translated(e);
         rational val;
         if (!mdl->eval_expr(r, r, true))
             return rational::zero();
@@ -1099,7 +465,7 @@ namespace intblast {
         }
 
         rational r, N = rational::power_of_two(bv.get_bv_size(e));
-        expr* te = translated(e);
+        expr* te = m_translator.translated(e);
         model_ref mdlr;
         m_solver->get_model(mdlr);
         expr_ref value(m);
@@ -1143,11 +509,11 @@ namespace intblast {
         return;
         for (auto n : ctx.get_egraph().nodes()) {
             auto e = n->get_expr();            
-            if (!is_translated(e))
+            if (!m_translator.is_translated(e))
                 continue;
             if (!bv.is_bv(e))
                 continue;
-            auto t = translated(e);
+            auto t = m_translator.translated(e);
             
             expr_ref ei(bv.mk_bv2int(e), m);
             expr_ref ti(a.mk_mod(t, a.mk_int(rational::power_of_two(bv.get_bv_size(e)))), m);
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index ee8d6fb19..d840e389f 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -38,6 +38,7 @@ Author:
 #include "solver/solver.h"
 #include "sat/smt/sat_th.h"
 #include "util/statistics.h"
+#include "ast/rewriter/bv2int_translator.h"
 
 namespace euf {
     class solver;
@@ -45,18 +46,31 @@ namespace euf {
 
 namespace intblast {
 
+    class translator_trail : public bv2int_translator_trail {
+        euf::solver& ctx;
+    public:
+        translator_trail(euf::solver& ctx):ctx(ctx) {}
+        void push(push_back_vector<expr_ref_vector> const& c) override;
+        void push(push_back_vector<ptr_vector<app>> const& c) override; 
+        void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) override; 
+    };
+
     class solver : public euf::th_euf_solver {
         euf::solver& ctx;
         sat::solver& s;
         ast_manager& m;
         bv_util bv;
         arith_util a;
+        translator_trail trail;
+        bv2int_translator m_translator;
+        
         scoped_ptr<::solver> m_solver;
-        obj_map<func_decl, func_decl*> m_new_funs;
-        expr_ref_vector m_translate, m_args;
-        ast_ref_vector m_pinned;
+
+        //obj_map<func_decl, func_decl*> m_new_funs;
+        //expr_ref_vector m_translate, m_args;
+        //ast_ref_vector m_pinned;
         sat::literal_vector m_core;
-        ptr_vector<app> m_bv2int, m_int2bv;
+        //        ptr_vector<app> m_bv2int, m_int2bv;
         statistics m_stats;
         bool m_is_plugin = true;        // when the solver is used as a plugin, then do not translate below quantifiers.        
 
@@ -66,33 +80,6 @@ namespace intblast {
 
 
 
-        bool is_translated(expr* e) const { return !!m_translate.get(e->get_id(), nullptr); }
-        expr* translated(expr* e) const { expr* r = m_translate.get(e->get_id(), nullptr); SASSERT(r); return r; }
-        void set_translated(expr* e, expr* r);
-        expr* arg(unsigned i) { return m_args.get(i); }
-
-        expr* umod(expr* bv_expr, unsigned i);
-        expr* smod(expr* bv_expr, unsigned i);
-        bool is_bounded(expr* v, rational const& N);
-        bool is_non_negative(expr* bv_expr, expr* e);
-        expr_ref mul(expr* x, expr* y);
-        expr_ref add(expr* x, expr* y);
-        expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
-        expr* amod(expr* bv_expr, expr* x, rational const& N);
-        rational bv_size(expr* bv_expr);
-
-        void translate_expr(expr* e);
-        void translate_bv(app* e);
-        void translate_basic(app* e);
-        void translate_app(app* e);
-        void translate_quantifier(quantifier* q);
-        void translate_var(var* v);
-
-        void ensure_translated(expr* e);
-        void internalize_bv(app* e);
-
-        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
-        ptr_vector<expr> m_vars, m_preds;
         bool add_bound_axioms();
         bool add_predicate_axioms();
 
@@ -101,6 +88,9 @@ namespace intblast {
         void add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values);
         void add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values);
 
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
+
+
     public:
         solver(euf::solver& ctx);
 
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 3922e9373..42469c365 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -61,6 +61,7 @@ z3_add_component(smt
     theory_dl.cpp
     theory_dummy.cpp
     theory_fpa.cpp
+    theory_intblast.cpp
     theory_lra.cpp
     theory_opt.cpp
     theory_pb.cpp
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index b227d9913..cb28d733a 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include "smt/theory_array.h"
 #include "smt/theory_array_full.h"
 #include "smt/theory_bv.h"
+#include "smt/theory_intblast.h"
 #include "smt/theory_datatype.h"
 #include "smt/theory_recfun.h"
 #include "smt/theory_dummy.h"
@@ -473,12 +474,12 @@ namespace smt {
     void setup::setup_QF_BV() {
         TRACE("setup", tout << "qf-bv\n";);
         m_params.setup_QF_BV();
-        m_context.register_plugin(alloc(smt::theory_bv, m_context));
+        setup_bv();
     }
 
     void setup::setup_QF_AUFBV() {
         m_params.setup_QF_AUFBV();
-        m_context.register_plugin(alloc(smt::theory_bv, m_context));
+        setup_bv();
         setup_arrays();
     }
 
@@ -695,7 +696,14 @@ namespace smt {
         family_id bv_fid = m_manager.mk_family_id("bv");
         if (m_context.get_theory(bv_fid))
             return;
-        switch(m_params.m_bv_mode) {
+        switch (m_params.m_bv_solver) {
+        case 2:
+            m_context.register_plugin(alloc(smt::theory_intblast, m_context));
+            return;
+        default:
+            break;
+        }
+        switch (m_params.m_bv_mode) {
         case BS_NO_BV:
             m_context.register_plugin(alloc(smt::theory_dummy, m_context, bv_fid, "no bit-vector"));
             break;
diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
new file mode 100644
index 000000000..e3b815a3d
--- /dev/null
+++ b/src/smt/theory_intblast.cpp
@@ -0,0 +1,148 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    theory_intblast
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-27
+
+--*/
+
+#include "smt/smt_context.h"
+#include "smt/theory_intblast.h"
+
+namespace smt {
+
+    void theory_intblast::translator_trail::push(push_back_vector<expr_ref_vector> const& c) {
+        ctx.push_trail(c);
+    }
+    void theory_intblast::translator_trail::push(push_back_vector<ptr_vector<app>> const& c) {
+        ctx.push_trail(c);
+    }
+    
+    void theory_intblast::translator_trail::push_idx(set_vector_idx_trail<expr_ref_vector> const& c) {
+        ctx.push_trail(c);
+    }
+
+    theory_intblast::theory_intblast(context& ctx):
+        theory(ctx, ctx.get_manager().mk_family_id("bv")),
+        m_trail(ctx),
+        m_translator(m, m_trail),
+        bv(m),
+        a(m)
+    {}
+    
+    theory_intblast::~theory_intblast() {}
+    
+    void theory_intblast::init() {
+        
+    }    
+    
+    final_check_status theory_intblast::final_check_eh() {
+        for (auto e : m_translator.bv2int()) {
+            auto* n = ctx.get_enode(e);
+            auto* r1 = n->get_arg(0)->get_root();
+            for (auto sib : *n) {
+                if (sib == n)
+                    continue;
+                if (!bv.is_bv2int(sib->get_expr()))
+                    continue;
+                if (sib->get_arg(0)->get_root() == r1)
+                    continue;
+                if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr()))
+                    continue;
+                auto a = mk_eq(n->get_expr(), sib->get_expr(), false);
+                auto b = mk_eq(sib->get_arg(0)->get_expr(), n->get_arg(0)->get_expr(), false);
+                ctx.mark_as_relevant(a);
+                ctx.mark_as_relevant(b);
+                ctx.mk_clause(~a, b, nullptr);
+                return final_check_status::FC_CONTINUE;
+            }
+        }
+        // ensure that int2bv respects values
+        // bv2int(int2bv(x)) = x mod N
+        for (auto e : m_translator.int2bv()) {
+            auto n = ctx.get_enode(e);
+            auto x = n->get_arg(0)->get_expr();
+            auto bv2int = bv.mk_bv2int(e);
+            ctx.internalize(bv2int, false);
+            auto N = rational::power_of_two(bv.get_bv_size(e));
+            auto xModN = a.mk_mod(x, a.mk_int(N));
+            ctx.internalize(xModN, false);
+            auto nBv2int = ctx.get_enode(bv2int);
+            auto nxModN = ctx.get_enode(xModN);
+            if (nBv2int->get_root() != nxModN->get_root()) {
+                auto a = mk_eq(nBv2int->get_expr(), nxModN->get_expr(), false);
+                ctx.mark_as_relevant(a);
+                ctx.mk_clause(1, &a, nullptr);
+                return final_check_status::FC_CONTINUE;
+            }
+        }
+        return final_check_status::FC_DONE;
+    }
+
+    bool theory_intblast::add_bound_axioms() {
+        auto const& vars = m_translator.vars();
+        if (m_vars_qhead == vars.size())
+            return false;
+        ctx.push_trail(value_trail(m_vars_qhead));
+        for (; m_vars_qhead < vars.size(); ++m_vars_qhead) {
+            auto v = vars[m_vars_qhead];
+            auto w = m_translator.translated(v);
+            auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort()));
+            auto lo = mk_literal(a.mk_ge(w, a.mk_int(0)));
+            auto hi = mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
+            ctx.mark_as_relevant(lo);
+            ctx.mark_as_relevant(hi);
+            ctx.mk_clause(1, &lo, nullptr);
+            ctx.mk_clause(1, &hi, nullptr);
+        }
+        return true;
+    }
+
+    bool theory_intblast::add_predicate_axioms() {
+        auto const& preds = m_translator.preds();
+        if (m_preds_qhead == preds.size())
+            return false;
+        ctx.push_trail(value_trail(m_preds_qhead));
+        for (; m_preds_qhead < preds.size(); ++m_preds_qhead) {
+            expr* e = preds[m_preds_qhead];
+            expr_ref r(m_translator.translated(e), m);
+            ctx.get_rewriter()(r);
+            auto a = mk_literal(e);
+            auto b = mk_literal(r);
+            ctx.mark_as_relevant(b);
+//            verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
+            ctx.mk_clause(~a, b, nullptr);
+            ctx.mk_clause(a, ~b, nullptr);
+        }
+        return true;
+    }
+
+    bool theory_intblast::can_propagate() {
+        return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size();
+    }
+
+    void theory_intblast::propagate() {
+        add_bound_axioms();
+        add_predicate_axioms();
+    }
+    
+    bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {
+        return internalize_term(atom);
+    }
+    
+    bool theory_intblast::internalize_term(app* term) {
+        m_translator.internalize_bv(term);
+        return true;
+    }
+    
+    void theory_intblast::internalize_eq_eh(app * atom, bool_var v) {
+        m_translator.translate_eq(atom);
+    }
+
+
+}
diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h
new file mode 100644
index 000000000..a3db28141
--- /dev/null
+++ b/src/smt/theory_intblast.h
@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    theory_intblast
+    
+Abstract:
+
+    Intblast version of bit-vector solver
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-10-24
+
+--*/
+#pragma once
+
+
+#include "util/rlimit.h"
+#include "ast/sls/sat_ddfw.h"
+#include "smt/smt_theory.h"
+#include "model/model.h"
+#include "ast/rewriter/bv2int_translator.h"
+
+
+namespace smt {
+
+    class theory_intblast : public theory {
+
+        class translator_trail : public bv2int_translator_trail {
+            context& ctx;
+        public:
+            translator_trail(context&  ctx):ctx(ctx) {}
+            void push(push_back_vector<expr_ref_vector> const& c) override;
+            void push(push_back_vector<ptr_vector<app>> const& c) override; 
+            void push_idx(set_vector_idx_trail<expr_ref_vector> const& c) override; 
+        };
+
+        translator_trail m_trail;
+        bv2int_translator m_translator;
+        bv_util           bv;
+        arith_util        a;
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
+
+        bool add_bound_axioms();
+        bool add_predicate_axioms();
+
+    public:
+        theory_intblast(context& ctx);
+        ~theory_intblast() override;
+
+        char const* get_name() const override { return "bv-intblast"; }
+        void init() override;
+        smt::theory* mk_fresh(context* new_ctx) override { return alloc(theory_intblast, *new_ctx); }
+        final_check_status final_check_eh() override;
+        void display(std::ostream& out) const override {}
+        bool can_propagate() override;
+        void propagate() override;
+        bool internalize_atom(app * atom, bool gate_ctx) override;
+        bool internalize_term(app* term) override;
+        void internalize_eq_eh(app * atom, bool_var v) override;
+        void new_eq_eh(theory_var v1, theory_var v2) override {}
+        void new_diseq_eh(theory_var v1, theory_var v2) override {}
+
+    };
+
+}
+
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c9ea77612..90fd207fc 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3276,6 +3276,8 @@ public:
             for (literal & c : m_core) {
                 c.neg();
                 ctx().mark_as_relevant(c);
+                if (ctx().get_assignment(c) == l_true)
+                    return;
             }
             TRACE("arith", ctx().display_literals_verbose(tout, m_core) << "\n";);
             ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data());