diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 0e3fa6ecb..39094b968 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -133,8 +133,26 @@ namespace intblast {
         return true;
     }
 
+    bool solver::add_bv2int_axioms() {
+        auto const& bv2int = m_translator.bv2int();
+        if (m_bv2int_qhead == bv2int.size())
+            return false;
+        ctx.push(value_trail(m_bv2int_qhead));
+        for (; m_bv2int_qhead < bv2int.size(); ++m_bv2int_qhead) {
+            app* e = bv2int[m_bv2int_qhead];
+            expr_ref r(m_translator.translated(e), m);
+            if (r.get() == e)
+                continue;
+            ctx.get_rewriter()(r);
+            auto lit = ctx.mk_literal(m.mk_eq(e, r));
+            ctx.mark_relevant(lit);
+            add_unit(lit);
+        }
+        return true;
+    }
+
     bool solver::unit_propagate() {
-        return add_bound_axioms() || add_predicate_axioms();
+        return add_bound_axioms() || add_predicate_axioms() || add_bv2int_axioms();
     }    
 
     lbool solver::check_axiom(sat::literal_vector const& lits) {
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index d840e389f..09f464544 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -82,13 +82,14 @@ namespace intblast {
 
         bool add_bound_axioms();
         bool add_predicate_axioms();
+        bool add_bv2int_axioms();
 
         euf::theory_var mk_var(euf::enode* n) override;
 
         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;
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0, m_bv2int_qhead = 0;
 
 
     public:
diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
index db244e6ed..1a17784b9 100644
--- a/src/smt/theory_intblast.cpp
+++ b/src/smt/theory_intblast.cpp
@@ -117,13 +117,33 @@ namespace smt {
         return true;
     }
 
+    bool theory_intblast::add_bv2int_axioms() {
+        auto const& bv2int = m_translator.bv2int();
+        if (m_bv2int_qhead == bv2int.size())
+            return false;
+        ctx.push_trail(value_trail(m_bv2int_qhead));
+        for (; m_bv2int_qhead < bv2int.size(); ++m_bv2int_qhead) {
+            app* e = bv2int[m_bv2int_qhead];
+            expr_ref r(m_translator.translated(e), m);
+            if (r.get() == e)
+                continue;
+            ctx.get_rewriter()(r);
+            auto eq = mk_eq(e, r, false);
+            ctx.mark_as_relevant(eq);
+            ctx.mk_th_axiom(m_id, 1, &eq);
+        }
+        return true;
+    }
+
     bool theory_intblast::can_propagate() {
-        return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size();
+        return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size() ||
+               m_bv2int_qhead < m_translator.bv2int().size();
     }
 
     void theory_intblast::propagate() {
         add_bound_axioms();
         add_predicate_axioms();
+        add_bv2int_axioms();
     }
     
     bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {
diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h
index 510e6b8f8..c629bb25d 100644
--- a/src/smt/theory_intblast.h
+++ b/src/smt/theory_intblast.h
@@ -42,11 +42,12 @@ namespace smt {
         bv2int_translator m_translator;
         bv_util           bv;
         arith_util        a;
-        unsigned m_vars_qhead = 0, m_preds_qhead = 0;
+        unsigned m_vars_qhead = 0, m_preds_qhead = 0, m_bv2int_qhead = 0;
         bv_factory *    m_factory = nullptr;
 
         bool add_bound_axioms();
         bool add_predicate_axioms();
+        bool add_bv2int_axioms();
 
     public:
         theory_intblast(context& ctx);