diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 308bc1326aa..3f094d43f08 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -401,6 +401,7 @@ class arith_util : public arith_recognizers {
 
     // return true if \c n is a term of the form (* -1 r)
     bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
+    bool is_one(expr const* n) const{ rational val; return is_numeral(n, val) && val.is_one(); }
     bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
     bool is_times_minus_one(expr* n, expr*& r) const {
         if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {
diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp
index 6631d9e5031..b4abe5e29d3 100644
--- a/src/ast/euf/euf_bv_plugin.cpp
+++ b/src/ast/euf/euf_bv_plugin.cpp
@@ -69,18 +69,15 @@ The formal properties of saturation have to be established.
 - Saturation does not complete with respect to associativity.
 Instead the claim is along the lines that the resulting E-graph can be used as a canonizer.
 If given a set of equations E that are saturated, and terms t1, t2 that are 
-both simplified with respect to left-associativity of concatenation, and t1, t2 belong to the E-graph,
+both simplified with respect to left-associativity of concatentation, and t1, t2 belong to the E-graph,
 then t1 = t2 iff t1 ~ t2 in the E-graph.
 
 TODO: Is saturation for (7) overkill for the purpose of canonization?
 
-TODO: revisit re-entrancy during register_node. It can be called when creating internal extract terms.
-Instead of allowing re-entrancy we can accumulate nodes that are registered during recursive calls 
-and have the main call perform recursive slicing.
-
 --*/
 
 
+#include "ast/ast_pp.h"
 #include "ast/euf/euf_bv_plugin.h"
 #include "ast/euf/euf_egraph.h"
 
@@ -91,19 +88,22 @@ namespace euf {
         bv(g.get_manager())
     {}
 
-    enode* bv_plugin::mk_value_concat(enode* a, enode* b) {
-        auto v1 = get_value(a);
-        auto v2 = get_value(b);
-        auto v3 = v1 + v2 * power(rational(2), width(a));
-        return mk_value(v3, width(a) + width(b));
+    enode* bv_plugin::mk_value_concat(enode* hi, enode* lo) {
+        auto v1 = get_value(hi);
+        auto v2 = get_value(lo);
+        auto v3 = v2 + v1 * rational::power_of_two(width(lo));
+        return mk_value(v3, width(lo) + width(hi));
     }
 
     enode* bv_plugin::mk_value(rational const& v, unsigned sz) {
         auto e = bv.mk_numeral(v, sz);
-        return mk(e, 0, nullptr);
+        auto n = mk(e, 0, nullptr);
+        if (m_ensure_th_var)
+            m_ensure_th_var(n);
+        return n;
     }
 
-    void bv_plugin::merge_eh(enode* x, enode* y) {
+    void bv_plugin::propagate_merge(enode* x, enode* y) {
         if (!bv.is_bv(x->get_expr()))
             return;
 
@@ -128,7 +128,36 @@ namespace euf {
             propagate_extract(n);
     }
 
-    // enforce concat(v1, v2) = v2*2^|v1| + v1
+    void bv_plugin::register_node(enode* n) { 
+        m_queue.push_back(n); 
+        m_trail.push_back(new (get_region()) push_back_vector(m_queue));  
+        push_plugin_undo(bv.get_family_id()); 
+    }
+
+    void bv_plugin::merge_eh(enode* n1, enode* n2) { 
+        m_queue.push_back(enode_pair(n1, n2)); 
+        m_trail.push_back(new (get_region()) push_back_vector(m_queue));  
+        push_plugin_undo(bv.get_family_id()); 
+    }
+
+    void bv_plugin::propagate() {
+        if (m_qhead == m_queue.size())
+            return;
+        m_trail.push_back(new (get_region()) value_trail(m_qhead));
+        push_plugin_undo(bv.get_family_id());
+        for (; m_qhead < m_queue.size(); ++m_qhead) {
+            if (std::holds_alternative<enode*>(m_queue[m_qhead])) {
+                auto n = *std::get_if<enode*>(&m_queue[m_qhead]);
+                propagate_register_node(n);
+            }
+            else {
+                auto [a, b] = *std::get_if<enode_pair>(&m_queue[m_qhead]);
+                propagate_merge(a, b);
+            }
+        }
+    }
+
+    // enforce concat(v1, v2) = v1*2^|v2| + v2
     void bv_plugin::propagate_values(enode* x) {
         if (!is_value(x))
             return;
@@ -142,9 +171,9 @@ namespace euf {
             if (is_concat(sib, a, b)) {
                 if (!is_value(a) || !is_value(b)) {
                     auto val = get_value(x);
-                    auto v1 = mod2k(val, width(a));
-                    auto v2 = machine_div2k(val, width(a));
-                    push_merge(mk_concat(mk_value(v1, width(a)), mk_value(v2, width(b))), x->get_interpreted());
+                    auto val_a = machine_div2k(val, width(b));
+                    auto val_b = mod2k(val, width(b));
+                    push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
                 }
             }
         }
@@ -176,18 +205,18 @@ namespace euf {
                 if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r)
                     return;
             // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications
-            push_merge(mk_concat(mk_extract(arg, lo, mid), mk_extract(arg, mid + 1, hi)), mk_extract(arg, lo, hi));
+            push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi));
         };
 
-        auto propagate_left = [&](enode* b) {
-            TRACE("bv", tout << "propagate-left " << g.bpp(b) << "\n");
+        auto propagate_above = [&](enode* b) {
+            TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n");
             for (enode* sib : enode_class(b))
                 if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2)
                     ensure_concat(lo1, hi1, hi2);
         };
 
-        auto propagate_right = [&](enode* a) {
-            TRACE("bv", tout << "propagate-right " << g.bpp(a) << "\n");
+        auto propagate_below = [&](enode* a) {
+            TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n");
             for (enode* sib : enode_class(a))
                 if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1)
                     ensure_concat(lo2, hi2, hi1);
@@ -196,46 +225,65 @@ namespace euf {
         for (enode* p : enode_parents(n)) {
             if (is_concat(p, a, b)) {
                 if (a->get_root() == n_r)
-                    propagate_left(b);
+                    propagate_below(b);
                 if (b->get_root() == n_r)
-                    propagate_right(a);
+                    propagate_above(a);
             }
         }
     }
 
-    void bv_plugin::push_undo_split(enode* n) { 
-        m_undo_split.push_back(n);
+    class bv_plugin::undo_split : public trail {
+        bv_plugin& p;
+        enode* n;
+    public:
+        undo_split(bv_plugin& p, enode* n): p(p), n(n) {}
+        void undo() override {
+            auto& i = p.info(n);
+            i.value = nullptr;
+            i.lo = nullptr;
+            i.hi = nullptr;
+            i.cut = null_cut;            
+        }
+    };
+
+    void bv_plugin::push_undo_split(enode* n) {
+        m_trail.push_back(new (get_region()) undo_split(*this, n));
         push_plugin_undo(bv.get_family_id());
     }
 
     void bv_plugin::undo() {
-        enode* n = m_undo_split.back();
-        m_undo_split.pop_back();
-        auto& i = info(n);
-        i.lo = nullptr;
-        i.hi = nullptr;
-        i.cut = null_cut;       
+        m_trail.back()->undo();
+        m_trail.pop_back();
     }
+
     
-    void bv_plugin::register_node(enode* n) {
+    void bv_plugin::propagate_register_node(enode* n) {
         TRACE("bv", tout << "register " << g.bpp(n) << "\n");
-        auto& i = info(n);
-        i.value = n;    
         enode* a, * b;
+        unsigned lo, hi;
         if (is_concat(n, a, b)) {
-            i.lo = a;
-            i.hi = b;
-            i.cut = width(a);
+            auto& i = info(n);
+            i.value = n;
+            i.hi = a;
+            i.lo = b;
+            i.cut = width(b);
             push_undo_split(n);
         }
-        unsigned lo, hi;
-        if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) {
+        else if (is_concat(n) && n->num_args() != 2) {
+            SASSERT(n->num_args() != 0);
+            auto last = n->get_arg(n->num_args() - 1);
+            for (unsigned i = n->num_args() - 1; i-- > 0;) 
+                last = mk_concat(n->get_arg(i), last);
+            push_merge(last, n);
+        }
+        else if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) {
             enode* arg = n->get_arg(0);   
             unsigned w = width(arg);
             if (all_of(enode_parents(arg), [&](enode* p) { unsigned _lo, _hi;  return !is_extract(p, _lo, _hi) || _lo != 0 || _hi + 1 != w; }))
                 push_merge(mk_extract(arg, 0, w - 1), arg);
             ensure_slice(arg, lo, hi);
         }
+        TRACE("bv", tout << "done register " << g.bpp(n) << "\n");
     }
 
     //
@@ -250,7 +298,8 @@ namespace euf {
             SASSERT(ub - lb + 1 == width(r));
             if (lb == lo && ub == hi)
                 return;
-            slice_info& i = info(r);
+            slice_info const& i = info(r);
+            
             if (!i.lo) {
                 if (lo > lb) {
                     split(r, lo - lb);
@@ -287,12 +336,20 @@ namespace euf {
             hi += lo1;
             n = n->get_arg(0);
         }
+        if (n->interpreted()) {
+            auto v = get_value(n);
+            if (lo > 0)
+                v = div(v, rational::power_of_two(lo));
+            if (hi + 1 != width(n))
+                v = mod(v, rational::power_of_two(hi + 1));
+            return mk_value(v, hi - lo + 1);
+        }
         return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n);
     }
 
-    enode* bv_plugin::mk_concat(enode* lo, enode* hi) { 
-        enode* args[2] = { lo, hi }; 
-        return mk(bv.mk_concat(lo->get_expr(), hi->get_expr()), 2, args); 
+    enode* bv_plugin::mk_concat(enode* hi, enode* lo) { 
+        enode* args[2] = { hi, lo }; 
+        return mk(bv.mk_concat(hi->get_expr(), lo->get_expr()), 2, args); 
     }
 
     void bv_plugin::merge(enode_vector& xs, enode_vector& ys, justification dep) {  
@@ -300,6 +357,7 @@ namespace euf {
             SASSERT(!ys.empty());
             auto x = xs.back();
             auto y = ys.back();
+            TRACE("bv", tout << "merge " << g.bpp(x) << " " << g.bpp(y) << "\n");
             if (unfold_sub(x, xs))
                 continue;
             else if (unfold_sub(y, ys))
@@ -342,14 +400,13 @@ namespace euf {
         SASSERT(0 < cut && cut < w);
         enode* hi = mk_extract(n, cut, w - 1);
         enode* lo = mk_extract(n, 0, cut - 1);        
-        auto& i = info(n);
-        if (!i.value)
-            i.value = n;
+        auto& i = info(n);        
+        i.value = n;
         i.hi = hi;
         i.lo = lo;
         i.cut = cut;
         push_undo_split(n);
-        push_merge(mk_concat(lo, hi), n);        
+        push_merge(mk_concat(hi, lo), n);        
     }
 
     void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
@@ -442,9 +499,12 @@ namespace euf {
                 continue;
             offsets.push_back(offs);
             if (n->get_root() == b->get_root() && offs == offset) {
+                if (n != b)
+                    consumer(n, b);
                 while (j != UINT_MAX) {
                     auto [x, y, j2] = just[j];
-                    consumer(x, y);
+                    if (x != y)
+                        consumer(x, y);
                     j = j2;
                 }
                 for (auto const& [n, offset, j] : m_jtodo) {
@@ -487,10 +547,10 @@ namespace euf {
     }
 
     std::ostream& bv_plugin::display(std::ostream& out) const {
-        out << "bv\n";
+        out << "bv\n";        
         for (auto const& i : m_info) 
-            if (i.lo)            
-                out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";        
+            if (i.lo)
+                out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";
         return out;
     }
 }
diff --git a/src/ast/euf/euf_bv_plugin.h b/src/ast/euf/euf_bv_plugin.h
index 199aed4e787..b90318c4d93 100644
--- a/src/ast/euf/euf_bv_plugin.h
+++ b/src/ast/euf/euf_bv_plugin.h
@@ -19,6 +19,7 @@ Module Name:
 
 #pragma once
 
+#include "util/trail.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/euf/euf_plugin.h"
 
@@ -40,26 +41,24 @@ namespace euf {
 
         bv_util                 bv;
         slice_info_vector       m_info;         // indexed by enode::get_id()
-
-
-
         enode_vector m_xs, m_ys;
 
+        std::function<void(enode*)> m_ensure_th_var;
+
         bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); }
-        bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && (a = n->get_arg(0), b = n->get_arg(1), true); }
+        bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && n->num_args() == 2 && (a = n->get_arg(0), b = n->get_arg(1), true); }
         bool is_extract(enode* n, unsigned& lo, unsigned& hi) { expr* body;  return bv.is_extract(n->get_expr(), lo, hi, body); }
         bool is_extract(enode* n) const { return bv.is_extract(n->get_expr()); }
         unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); }        
 
         enode* mk_extract(enode* n, unsigned lo, unsigned hi);
-        enode* mk_concat(enode* lo, enode* hi);
-        enode* mk_value_concat(enode* lo, enode* hi);
+        enode* mk_concat(enode* hi, enode* lo);
+        enode* mk_value_concat(enode* hi, enode* lo);
         enode* mk_value(rational const& v, unsigned sz);
         unsigned width(enode* n) { return bv.get_bv_size(n->get_expr()); }
         bool  is_value(enode* n) { return n->get_root()->interpreted(); }
         rational get_value(enode* n) { rational val; VERIFY(bv.is_numeral(n->get_interpreted()->get_expr(), val)); return val; }
         slice_info& info(enode* n) { unsigned id = n->get_id(); m_info.reserve(id + 1); return m_info[id]; }
-        slice_info& root_info(enode* n) { unsigned id = n->get_root_id(); m_info.reserve(id + 1); return m_info[id]; }
         bool has_sub(enode* n) { return !!info(n).lo; }
         enode* sub_lo(enode* n) { return info(n).lo; }
         enode* sub_hi(enode* n) { return info(n).hi; }
@@ -81,8 +80,16 @@ namespace euf {
         svector<std::tuple<enode*, unsigned, unsigned>> m_jtodo;
         void clear_offsets();
 
-        enode_vector m_undo_split;
+
+        ptr_vector<trail> m_trail;
+        
+        class undo_split;
         void push_undo_split(enode* n);
+
+        vector<std::variant<enode*, enode_pair>> m_queue;
+        unsigned m_qhead = 0;        
+        void propagate_register_node(enode* n);
+        void propagate_merge(enode* a, enode* b);
         
     public:
         bv_plugin(egraph& g);
@@ -97,9 +104,11 @@ namespace euf {
 
         void diseq_eh(enode* eq) override {}
 
-        void propagate() override {}
+        void propagate() override;
 
         void undo() override;
+
+        void set_ensure_th_var(std::function<void(enode*)>& f) { m_ensure_th_var = f; }
         
         std::ostream& display(std::ostream& out) const override;
 
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index c32a8173933..12f81721258 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -107,6 +107,8 @@ namespace euf {
     void egraph::update_children(enode* n) {
         for (enode* child : enode_args(n)) 
             child->get_root()->add_parent(n);
+        for (enode* child : enode_args(n))  
+            SASSERT(child->get_root()->m_parents.back() == n);
         m_updates.push_back(update_record(n, update_record::update_children()));
     }
 
@@ -158,7 +160,7 @@ namespace euf {
     }
 
     void egraph::add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) {
-        TRACE("euf_verbose", tout << "eq: " << v1 << " == " << v2 << "\n";);
+        TRACE("euf", tout << "eq: " << v1 << " == " << v2 << " - " << bpp(c) << " == " << bpp(r) << "\n";);
         m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r));
         m_updates.push_back(update_record(update_record::new_th_eq()));
         ++m_stats.m_num_th_eqs;
@@ -442,6 +444,8 @@ namespace euf {
                 break;
             case update_record::tag_t::is_update_children:
                 for (unsigned i = 0; i < p.r1->num_args(); ++i) {
+                    CTRACE("euf", (p.r1->m_args[i]->get_root()->m_parents.back() != p.r1),
+                           display(tout << bpp(p.r1->m_args[i]) << " " << bpp(p.r1->m_args[i]->get_root()) << " "););
                     SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1);
                     p.r1->m_args[i]->get_root()->m_parents.pop_back();
                 }
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index dd6c9b9da22..8822b07e793 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -192,8 +192,8 @@ namespace euf {
         enode_vector           m_empty_enodes;
         unsigned               m_num_scopes = 0;
         bool                   m_inconsistent = false;
-        enode*                 m_n1 = nullptr;
-        enode*                 m_n2 = nullptr;
+        enode                  *m_n1 = nullptr;
+        enode                  *m_n2 = nullptr;
         justification          m_justification;
         unsigned               m_new_th_eqs_qhead = 0;
         svector<th_eq>         m_new_th_eqs;
@@ -205,11 +205,11 @@ namespace euf {
         uint64_t               m_congruence_timestamp = 0;
 
         std::vector<std::function<void(enode*,enode*)>> m_on_merge;
-        std::function<void(enode*,enode*)>              m_on_propagate_literal;
-        std::function<void(enode*)>                     m_on_make;
-        std::function<void(expr*,expr*,expr*)>          m_used_eq;
-        std::function<void(app*,app*)>                  m_used_cc;
-        std::function<void(std::ostream&,void*)>        m_display_justification;
+        std::function<void(enode*, enode*)>    m_on_propagate_literal;
+        std::function<void(enode*)>            m_on_make;
+        std::function<void(expr*,expr*,expr*)> m_used_eq;
+        std::function<void(app*,app*)>         m_used_cc;  
+        std::function<void(std::ostream&, void*)>   m_display_justification;
 
         void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
             m_updates.push_back(update_record(r1, n1, r2_num_parents));
@@ -218,7 +218,7 @@ namespace euf {
 
         // plugin related methods
         void push_plugin_undo(unsigned th_id) { m_updates.push_back(update_record(th_id, update_record::plugin_undo())); }
-        void push_merge(enode* a, enode* b, justification j) { m_to_merge.push_back({ a, b, j }); }
+        void push_merge(enode* a, enode* b, justification j) { SASSERT(a->get_sort() == b->get_sort());  m_to_merge.push_back({ a, b, j }); }
         void push_merge(enode* a, enode* b, bool comm) { m_to_merge.push_back({ a, b, comm }); }
         void propagate_plugins();
 
@@ -279,6 +279,7 @@ namespace euf {
         void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }        
         void new_diseq(enode* n);
 
+
         /**
            \brief propagate set of merges. 
            This call may detect an inconsistency. Then inconsistent() is true.
@@ -325,13 +326,13 @@ namespace euf {
         void set_relevant(enode* n);
         void set_default_relevant(bool b) { m_default_relevant = b; }
 
-        void set_on_merge(std::function<void(enode* root,enode* other)> on_merge) { m_on_merge.push_back(std::move(on_merge)); }
-        void set_on_propagate(std::function<void(enode* lit,enode* ante)> on_propagate) { m_on_propagate_literal = std::move(on_propagate); }
-        void set_on_make(std::function<void(enode* n)> on_make) { m_on_make = std::move(on_make); }
-        void set_used_eq(std::function<void(expr*,expr*,expr*)> used_eq) { m_used_eq = std::move(used_eq); }
-        void set_used_cc(std::function<void(app*,app*)> used_cc) { m_used_cc = std::move(used_cc); }
-        void set_display_justification(std::function<void(std::ostream&, void*)> d) { m_display_justification = std::move(d); }
-
+        void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
+        void set_on_propagate(std::function<void(enode* lit,enode* ante)>& on_propagate) { m_on_propagate_literal = on_propagate; }
+        void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
+        void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
+        void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
+        void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; }
+        
         void begin_explain();
         void end_explain();
         bool uses_congruence() const { return m_uses_congruence; }
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 20bc7826057..b2dd5e96908 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -260,9 +260,6 @@ namespace arith {
             if (valy >= sz || valy == 0)
                 return true;
             unsigned k = valy.get_unsigned();
-            rational r = mod(valx * rational::power_of_two(k), N);
-            if (r == valn)
-                return true;
             sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)));
             if (s().value(eq) == l_true)
                 return true;            
@@ -275,9 +272,6 @@ namespace arith {
             if (valy >= sz || valy == 0)
                 return true;
             unsigned k = valy.get_unsigned();
-            rational r = mod(div(valx, rational::power_of_two(k)), N);
-            if (r == valn)
-                return true;
             sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))));
             if (s().value(eq) == l_true)
                 return true;            
@@ -290,12 +284,6 @@ namespace arith {
             if (valy >= sz || valy == 0)
                 return true;
             unsigned k = valy.get_unsigned();
-            bool signvalx = x >= N/2;
-            rational valxdiv2k = div(valx, rational::power_of_two(k));
-            if (signvalx)
-                valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N);
-            if (valn == valxdiv2k)
-                return true;
             sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
             sat::literal eq;
             expr* xdiv2k;
@@ -334,11 +322,7 @@ namespace arith {
         return true;
     }
 
-    /*
-    * 0 <= x&y < 2^sz
-    * x&y <= x
-    * x&y <= y
-    */
+
     void solver::mk_bv_axiom(app* n) {
         unsigned sz;
         expr* _x, * _y;
@@ -347,10 +331,15 @@ namespace arith {
         expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
         expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
 
-        add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
-        add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
-
         if (a.is_band(n)) {
+            
+            // 0 <= x&y < 2^sz
+            // x&y <= x
+            // x&y <= y
+            // TODO? x = y => x&y = x
+
+            add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
+            add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
             add_clause(mk_literal(a.mk_le(n, x)));
             add_clause(mk_literal(a.mk_le(n, y)));
         }
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index f8a7beed0d4..2c373f6b935 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -37,6 +37,7 @@ namespace intblast {
     euf::theory_var solver::mk_var(euf::enode* n) {
         auto r = euf::th_euf_solver::mk_var(n);
         ctx.attach_th_var(n, this, r);
+        TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";);
         return r;
     }
 
@@ -97,16 +98,16 @@ namespace intblast {
             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)));            
+            set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
         }
         m_preds.push_back(e);
         ctx.push(push_back_vector(m_preds));
     }
 
-    void solver::set_translated(expr* e, expr* r) {
+    void solver::set_translated(expr* e, expr* r) { 
         SASSERT(r);
-        SASSERT(!is_translated(e));
-        m_translate.setx(e->get_id(), r);
+        SASSERT(!is_translated(e));          
+        m_translate.setx(e->get_id(), r); 
         ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
     }
 
@@ -147,7 +148,7 @@ namespace intblast {
             auto a = expr2literal(e);
             auto b = mk_literal(r);
             ctx.mark_relevant(b);
-            TRACE("intblast", tout << "add-predicate-axiom: " << mk_bounded_pp(e, m) << " \n" << r << "\n");
+//            verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
             add_equiv(a, b);
         }
         return true;
@@ -156,7 +157,6 @@ 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;
@@ -178,10 +178,96 @@ namespace intblast {
                 }
         }
         std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
-        for (expr* e : todo)
+        for (expr* e : todo)            
             translate_expr(e);
     }
 
+    lbool solver::check_axiom(sat::literal_vector const& lits) {
+        sat::literal_vector core;
+        for (auto lit : lits)
+            core.push_back(~lit);
+        return check_core(core, {});
+    }
+    lbool solver::check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
+        sat::literal_vector core;
+        core.append(lits);
+        core.push_back(~lit);
+        return check_core(core, eqs);
+    }
+
+    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_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));
+        for (auto [a, b] : eqs)
+            es.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
+        
+        original_es.append(es);
+
+        lbool r;
+        if (false) {
+            r = m_solver->check_sat(es);            
+        }
+        else {
+        
+            translate(es);
+            
+            for (auto e : m_vars) {
+                auto v = 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)));
+            }
+
+            for (unsigned i = 0; i < es.size(); ++i) {
+                expr_ref tmp(es.get(i), m);
+                ctx.get_rewriter()(tmp);
+                es[i] = tmp;
+            }
+
+            IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n");
+            
+            IF_VERBOSE(2,
+                {
+                    m_solver->push();
+                    m_solver->assert_expr(es);
+                    m_solver->display(verbose_stream()) << "(check-sat)\n";
+                    m_solver->pop(1);
+                });
+
+            
+            r = m_solver->check_sat(es);
+        }
+
+        m_solver->collect_statistics(m_stats);
+
+        IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
+        if (r == l_true) {
+            IF_VERBOSE(0,
+                model_ref mdl;
+                m_solver->get_model(mdl);
+                verbose_stream() << original_es << "\n";
+                verbose_stream() << *mdl << "\n";
+                verbose_stream() << es << "\n";
+                m_solver->display(verbose_stream()););
+            SASSERT(false);
+        }
+
+        m_solver = nullptr;
+
+        return r;
+    }
+
+    
+
     lbool solver::check_solver_state() {
         sat::literal_vector literals;
         uint_set selected;
@@ -291,6 +377,8 @@ namespace intblast {
         for (expr* e : es) {
             if (is_translated(e))
                 continue;
+            if (visited.is_marked(e))
+                continue;
             sorted.push_back(e);
             visited.mark(e);
         }
@@ -304,6 +392,7 @@ namespace intblast {
                         sorted.push_back(arg);
                     }
                 }
+
             }
             else if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
@@ -334,7 +423,7 @@ namespace intblast {
             es[i] = translated(es.get(i));
     }
 
-    sat::check_result solver::check() {
+    sat::check_result solver::check() { 
         // ensure that bv2int is injective
         for (auto e : m_bv2int) {
             euf::enode* n = expr2enode(e);
@@ -346,12 +435,10 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
-                if (sib->get_arg(0)->get_sort() != n->get_arg(0)->get_sort())
-                    continue;
-                auto a = eq_internalize(n, sib);
-                auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
-                ctx.mark_relevant(a);
-                ctx.mark_relevant(b);
+		auto a = eq_internalize(n, sib);
+		auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
+		ctx.mark_relevant(a);
+		ctx.mark_relevant(b);
                 add_clause(~a, b, nullptr);
                 return sat::check_result::CR_CONTINUE;
             }
@@ -369,27 +456,40 @@ namespace intblast {
             auto nBv2int = ctx.get_enode(bv2int);
             auto nxModN = ctx.get_enode(xModN);
             if (nBv2int->get_root() != nxModN->get_root()) {
-                auto a = eq_internalize(nBv2int, nxModN);
-                ctx.mark_relevant(a);
-                add_unit(a);
-                return sat::check_result::CR_CONTINUE;
+	      auto a = eq_internalize(nBv2int, nxModN);
+	      ctx.mark_relevant(a);
+              add_unit(a);
+              return sat::check_result::CR_CONTINUE;
             }
         }
-        return sat::check_result::CR_DONE;
+        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.get_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, * y;
+        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 r;
         rational N = bv_size(bv_expr);
-        if (a.is_numeral(x, r)) {
-            if (0 <= r && r < N)
-                return x;
-            return a.mk_int(mod(r, N));
-        }
-        if (any_of(m_vars, [&](expr* v) { return translated(v) == x && bv.get_bv_size(v) == bv.get_bv_size(bv_expr); }))
-            return x;
-        return a.mk_mod(x, a.mk_int(N));
+        return amod(bv_expr, x, N);
     }
 
     expr* solver::smod(expr* bv_expr, unsigned i) {
@@ -399,7 +499,61 @@ namespace intblast {
         rational r;
         if (a.is_numeral(x, r))
             return a.mk_int(mod(r + shift, N));
-        return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(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 dose not disappear.
+    */
+    expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
+        rational v;
+        expr* r, *c, * t, * e;
+        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) {
@@ -483,8 +637,7 @@ namespace intblast {
                 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);
-
+            m_vars.push_back(e);        
         if (m_is_plugin) {
             expr* r = m.mk_app(f, m_args);
             if (has_bv_sort) {
@@ -505,7 +658,7 @@ namespace intblast {
             f = g;
             m_pinned.push_back(f);
         }
-        set_translated(e, m.mk_app(f, m_args));
+        set_translated(e, m.mk_app(f, m_args));        
     }
 
     void solver::translate_bv(app* e) {
@@ -532,15 +685,15 @@ namespace intblast {
                 auto N = bv_size(e);
                 auto A = rational::power_of_two(sz - n);
                 auto B = rational::power_of_two(n);
-                auto hi = a.mk_mul(r, a.mk_int(A));
-                auto lo = a.mk_mod(a.mk_idiv(umod(e, 0), a.mk_int(B)), a.mk_int(A));
-                r = a.mk_add(hi, lo);
+                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* r = nullptr;
+        expr_ref r(m);
         auto const& args = m_args;
         switch (e->get_decl_kind()) {
         case OP_BADD:
@@ -573,7 +726,6 @@ namespace intblast {
             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:
@@ -589,12 +741,13 @@ namespace intblast {
             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);
-                expr* new_arg = umod(old_arg, i);
+                new_arg = umod(old_arg, i);
                 if (sz > 0) {
-                    new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz)));
-                    r = a.mk_add(r, new_arg);
+                    new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
+                    r = add(r, new_arg);
                 }
                 else
                     r = new_arg;
@@ -606,10 +759,9 @@ namespace intblast {
             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(umod(old_arg, 0), a.mk_int(rational::power_of_two(lo)));
-            else 
-                r = arg(0);
+                r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
             break;
         }
         case OP_BV_NUM: {
@@ -627,32 +779,32 @@ namespace intblast {
         }
         case OP_BUDIV:
         case OP_BUDIV_I: {
-            expr* x = umod(e, 0), * y = umod(e, 1);
+            expr* x = arg(0), * y = umod(e, 1);
             r = m.mk_ite(m.mk_eq(y, a.mk_int(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(a.mk_mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
+            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));
+            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 = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r);
+                    r = m.mk_ite(m.mk_eq(y, a.mk_int(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)))
+        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);
@@ -662,11 +814,11 @@ namespace intblast {
                     r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
             }
             break;
-        case OP_BASHR:
+        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   
@@ -674,15 +826,15 @@ namespace intblast {
                 //
                 unsigned sz = bv.get_bv_size(e);
                 rational N = bv_size(e);
-                expr* x = umod(e, 0), * y = umod(e, 1);
+                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));
+                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)));
+                    expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));              
                     r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
-                        m.mk_ite(signx, a.mk_add(d, a.mk_int(-rational::power_of_two(sz - i))), d),
-                        r);
+                                 m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
+                                 r);
                 }
             }
             break;
@@ -691,7 +843,7 @@ namespace intblast {
             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(a.mk_add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
+                r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
             break;
         }
         case OP_BNAND:
@@ -709,7 +861,7 @@ namespace intblast {
             r = arg(0);
             for (unsigned i = 1; i < args.size(); ++i) {
                 expr* q = arg(i);
-                r = a.mk_sub(a.mk_add(r, q), a.mk_mul(a.mk_int(2), a.mk_band(sz, r, q)));
+                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);
@@ -747,11 +899,11 @@ namespace intblast {
             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));
+        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
@@ -759,14 +911,14 @@ namespace intblast {
             // 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), a.mk_add(u, y), r);
+            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 = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r);
             r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
             break;
-        }
+        } 
         case OP_BSDIV_I:
         case OP_BSDIV: {
             // d = udiv(abs(x), abs(y))
@@ -800,9 +952,9 @@ namespace intblast {
             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, a.mk_mul(d, y));
+            r = a.mk_sub(x, mul(d, y));
             r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
-            break;
+            break;  
         }
         case OP_ROTATE_LEFT: {
             auto n = e->get_parameter(0).get_int();
@@ -815,11 +967,11 @@ namespace intblast {
             r = rotate_left(sz - n);
             break;
         }
-        case OP_EXT_ROTATE_LEFT: {
+        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)
+            for (unsigned i = 0; i < sz; ++i) 
                 r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r);
             break;
         }
@@ -827,7 +979,7 @@ namespace intblast {
             unsigned sz = bv.get_bv_size(e);
             expr* y = umod(e, 1);
             r = a.mk_int(0);
-            for (unsigned i = 0; i < sz; ++i)
+            for (unsigned i = 0; i < sz; ++i) 
                 r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r);
             break;
         }
@@ -838,9 +990,9 @@ namespace intblast {
             rational N = bv_size(e->get_arg(0));
             rational N0 = N;
             for (unsigned i = 1; i < n; ++i)
-                r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0;
+                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)));
@@ -864,8 +1016,15 @@ namespace intblast {
             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);
-                m_args[0] = a.mk_sub(arg(0), arg(1));
-                set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(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)));
@@ -874,8 +1033,8 @@ namespace intblast {
             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));
+        else 
+            set_translated(e, m.mk_app(e->get_decl(), m_args));        
     }
 
     rational solver::get_value(expr* e) const {
@@ -903,12 +1062,6 @@ namespace intblast {
         if (!is_app(n->get_expr()))
             return false;
         app* e = to_app(n->get_expr());
-        expr *th, * el, * c;
-        if (m.is_ite(e, c, th, el)) {
-            dep.add(n, expr2enode(th)->get_root());
-            dep.add(n, expr2enode(el)->get_root());
-            return true;
-        }
         if (n->num_args() == 0) {
             dep.insert(n, nullptr);
             return true;
@@ -925,7 +1078,6 @@ namespace intblast {
     void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) {
         expr* e = n->get_expr();
         SASSERT(bv.is_bv(e));
-
         if (bv.is_numeral(e)) {
             values.setx(n->get_root_id(), e);
             return;
@@ -947,15 +1099,6 @@ namespace intblast {
 
     void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) {
         expr_ref value(m);
-        expr* e = n->get_expr(), *c, *th, *el;
-        while (m.is_ite(e, c, th, el)) {
-            auto thn = expr2enode(th);
-            if (thn->get_root() == n->get_root())
-                e = th;
-            else
-                e = el;
-            n = expr2enode(e);
-        }        
         if (n->interpreted())
             value = n->get_expr();
         else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {
@@ -975,35 +1118,12 @@ namespace intblast {
             rational r;
             VERIFY(av.get_value(b2i->get_expr(), r));
             value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
+            verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
         }
         values.set(n->get_root_id(), value);
         TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
     }
 
-    void solver::finalize_model(model& mdl) {
-        for (auto n : ctx.get_egraph().nodes()) {
-            expr* e = n->get_expr();
-            if (!bv.is_bv(e))
-                continue;
-            if (!is_translated(e))
-                continue;
-            expr* f = translated(e);
-            rational r1, r2;
-            expr_ref val1 = mdl(e);
-            expr_ref val2 = mdl(f);
-            if (bv.is_numeral(val1, r1) && a.is_numeral(val2, r2) && r1 != r2) {
-                rational N = rational::power_of_two(bv.get_bv_size(e));
-                r2 = mod(r2, N);
-                if (r1 == r2)
-                    continue;
-                verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n";
-                verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n";
-                for (expr* arg : *to_app(e)) 
-                    verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n";
-            }
-        }
-    }
-
     sat::literal_vector const& solver::unsat_core() {
         return m_core;
     }
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index 1739fc09bbf..0aceb8b2bb6 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -73,6 +73,11 @@ namespace intblast {
 
         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* amod(expr* bv_expr, expr* x, rational const& N);
         rational bv_size(expr* bv_expr);
 
         void translate_expr(expr* e);
@@ -100,6 +105,10 @@ namespace intblast {
         
         ~solver() override {}
 
+        lbool check_axiom(sat::literal_vector const& lits);
+        lbool check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
+        lbool check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
+
         lbool check_solver_state();
 
         sat::literal_vector const& unsat_core();
@@ -108,8 +117,6 @@ namespace intblast {
 
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
 
-        void finalize_model(model& mdl) override;
-
         std::ostream& display(std::ostream& out) const override;
 
         void collect_statistics(statistics& st) const override;