diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 4df9efa6f..308bc1326 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -309,14 +309,13 @@ public:
     bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }
 
     bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); }
-    bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) {
-        if (!is_band(n))
-            return false;
-        x = to_app(n)->get_arg(0);
-        y = to_app(n)->get_arg(1);
-        sz = to_app(n)->get_parameter(0).get_int();
-        return true;
-    }
+    bool is_band(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_BAND, sz, x, y); }
+    bool is_shl(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_SHL); }
+    bool is_shl(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_SHL, sz, x, y); }
+    bool is_lshr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_LSHR); }
+    bool is_lshr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_LSHR, sz, x, y); }
+    bool is_ashr(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_ASHR); }
+    bool is_ashr(expr const* n, unsigned& sz, expr*& x, expr*& y) { return is_arith_op(n, OP_ARITH_ASHR, sz, x, y); }
 
     bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); }
     bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); }
diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h
index 50339e3ce..021501ecd 100644
--- a/src/math/lp/lp_api.h
+++ b/src/math/lp/lp_api.h
@@ -129,11 +129,7 @@ namespace lp_api {
             st.update("arith-gomory-cuts", m_gomory_cuts);
             st.update("arith-assume-eqs", m_assume_eqs);
             st.update("arith-branch", m_branch);
-<<<<<<< HEAD
             st.update("arith-bv-axioms", m_bv_axioms);
-=======
-            st.update("arith-band-axioms", m_band_axioms);
->>>>>>> c72780d9b (b-and, stats, reinsert variable to heap, debugging)
         }
     };
 
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index a9206ef4e..cbf4206a9 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -410,13 +410,8 @@ namespace arith {
         bool  check_delayed_eqs();
         lbool check_lia();
         lbool check_nla();
-<<<<<<< HEAD
         bool check_bv_terms();
         bool check_bv_term(app* n);
-=======
-        bool check_band_terms();
-        bool check_band_term(app* n);
->>>>>>> b72575148 (axioms for b-and)
         void add_lemmas();
         void propagate_nla();
         void add_equality(lpvar v, rational const& k, lp::explanation const& exp);
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 4b05abc3d..6ab6e67fd 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -104,10 +104,10 @@ namespace intblast {
         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()));
     }
 
@@ -148,7 +148,7 @@ namespace intblast {
             auto a = expr2literal(e);
             auto b = mk_literal(r);
             ctx.mark_relevant(b);
-            //            verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
+//            verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
             add_equiv(a, b);
         }
         return true;
@@ -157,7 +157,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;
@@ -179,7 +179,7 @@ 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);
     }
 
@@ -305,6 +305,28 @@ namespace intblast {
                         sorted.push_back(arg);
                     }
                 }
+
+                //
+                // Add ground equalities to ensure the model is valid with respect to the current case splits.
+                // This may cause more conflicts than necessary. Instead could use intblast on the base level, but using literal
+                // assignment from complete level.
+                // E.g., force the solver to completely backtrack, check satisfiability using the assignment obtained under a complete assignment.
+                // If intblast is SAT, then force the model and literal assignment on the rest of the literals.
+                // 
+                if (!is_ground(e))
+                    continue;
+                euf::enode* n = ctx.get_enode(e);
+                if (!n)
+                    continue;
+                if (n == n->get_root())
+                    continue;
+                expr* r = n->get_root()->get_expr();
+                es.push_back(m.mk_eq(e, r));
+                r = es.back();
+                if (!visited.is_marked(r) && !is_translated(r)) {
+                    visited.mark(r);
+                    sorted.push_back(r);
+                }
             }
             else if (is_quantifier(e)) {
                 quantifier* q = to_quantifier(e);
@@ -325,6 +347,7 @@ namespace intblast {
 
         for (expr* e : todo)
             translate_expr(e);
+
         TRACE("bv",
             for (expr* e : es)
                 tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated(e), m) << "\n";
@@ -334,7 +357,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,10 +369,10 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     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;
             }
@@ -367,13 +390,13 @@ 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);
+	      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; 
     }
 
     expr* solver::umod(expr* bv_expr, unsigned i) {
@@ -481,8 +504,8 @@ 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) {
@@ -503,7 +526,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) {
@@ -535,7 +558,7 @@ namespace intblast {
                 r = a.mk_add(hi, lo);
             }
             return r;
-            };
+        };
 
         expr* bv_expr = e;
         expr* r = nullptr;
@@ -682,7 +705,6 @@ namespace intblast {
                 }
             }
             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");
@@ -744,11 +766,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
@@ -756,14 +778,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 = a.mk_uminus(u);   
             r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_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))
@@ -799,7 +821,7 @@ namespace intblast {
             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 = 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();
@@ -812,11 +834,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;
         }
@@ -824,7 +846,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;
         }
@@ -837,7 +859,7 @@ namespace intblast {
             for (unsigned i = 1; i < n; ++i)
                 r = a.mk_add(a.mk_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)));
@@ -855,6 +877,7 @@ namespace intblast {
         }
         set_translated(e, r);
     }
+
     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); });
@@ -896,7 +919,7 @@ namespace intblast {
     }
 
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
-        if (!is_app(n->get_expr()))
+      if (!is_app(n->get_expr()))
             return false;
         app* e = to_app(n->get_expr());
         if (n->num_args() == 0) {
@@ -915,7 +938,7 @@ 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;
@@ -955,8 +978,8 @@ namespace intblast {
             arith::arith_value av(ctx);
             rational r;
             VERIFY(av.get_value(b2i->get_expr(), r));
-            verbose_stream() << ctx.bpp(n) << " := " << r << "\n";
             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");
diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h
index e6f82f7cf..d59dac935 100644
--- a/src/sat/smt/intblast_solver.h
+++ b/src/sat/smt/intblast_solver.h
@@ -66,35 +66,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);
-        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();
-
-        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);
-
         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);
@@ -165,10 +136,7 @@ namespace intblast {
 
         void eq_internalized(euf::enode* n) override;
 
-        sat::literal_vector const& unsat_core();
-
-        void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
-
+        rational get_value(expr* e) const;
 
     };