diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h
index 308bc1326..4df9efa6f 100644
--- a/src/ast/arith_decl_plugin.h
+++ b/src/ast/arith_decl_plugin.h
@@ -309,13 +309,14 @@ 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) { 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_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_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/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 078515184..02849a8eb 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1212,6 +1212,8 @@ namespace arith {
         default:
             UNREACHABLE();
         }
+        if (lia_check == l_true && !check_band_terms())
+            lia_check = l_false;
         return lia_check;
     }
 
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index cbf4206a9..a9206ef4e 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -410,8 +410,13 @@ 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 2401499b9..09241d42b 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -237,7 +237,6 @@ namespace intblast {
         m_core.reset();
         m_vars.reset();
         m_trail.reset();
-        m_new_funs.reset();
         m_solver = mk_smt2_solver(m, s.params(), symbol::null);
 
         expr_ref_vector es(m);
@@ -325,7 +324,6 @@ 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";