diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 736218bc4..b2207199c 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -97,30 +97,6 @@ namespace smt {
             // This will also force the creation of all bits for x.
             enode * first_arg_enode = ctx.get_enode(first_arg);
             get_var(first_arg_enode);
-#if 0
-            // constant axiomatization moved to catch all case in the end of function.
-
-            // numerals are not blasted into bit2bool, so we do this directly.
-            rational val;
-            unsigned sz;
-            if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
-                
-                TRACE("bv", tout << "bit2bool constants\n";);
-                theory_var v = first_arg_enode->get_th_var(get_id());
-                app* owner = first_arg_enode->get_owner();
-                for (unsigned i = 0; i < sz; ++i) {
-                    app* e = mk_bit2bool(owner, i);
-                    ctx.internalize(e, true);
-                }
-                m_bits[v].reset();
-                rational bit;                
-                for (unsigned i = 0; i < sz; ++i) {
-                    div(val, rational::power_of_two(i), bit);
-                    mod(bit, rational(2), bit);
-                    m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);                                        
-                }
-            }
-#endif
         }
          
         enode * arg      = ctx.get_enode(first_arg);
@@ -144,6 +120,13 @@ namespace smt {
             unsigned idx     = n->get_decl()->get_parameter(0).get_int();
             SASSERT(a->m_occs == 0);
             a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
+#if 0
+            // possible fix for #2162, but effect of fix needs to be checked.
+            if (idx < m_bits[v_arg].size()) {
+                ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true));
+                ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false));
+            }      
+#endif      
         }
         // axiomatize bit2bool on constants.
         rational val;
@@ -782,6 +765,7 @@ namespace smt {
             bits.swap(new_bits);                                                                \
         }                                                                                       \
         init_bits(e, bits);                                                                     \
+        TRACE("bv", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \
     }
 
 
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 9e941fcd5..dd1b302e1 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -175,7 +175,7 @@ namespace smt {
         unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0;
         unsigned i = 0;
         for (func_decl * acc : accessors) {
-            app * acc_app     = m.mk_app(acc, n->get_owner());
+            app_ref acc_app(m.mk_app(acc, n->get_owner()), m);
             enode * arg       = n->get_arg(i);
             if (m.has_trace_stream()) {
                 app_ref body(m);
@@ -239,7 +239,7 @@ namespace smt {
                 ctx.internalize(acc_app, false);
                 arg = ctx.get_enode(acc_app);
             }
-            app * acc_own = m.mk_app(acc1, own);
+            app_ref acc_own(m.mk_app(acc1, own), m);
             if (m.has_trace_stream()) {
                 app_ref body(m);
                 body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
@@ -249,8 +249,7 @@ namespace smt {
             if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }
         // update_field is identity if 'n' is not created by a matching constructor.        
-        app_ref imp(m);
-        imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1));
+        app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1)), m);
         if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
         assert_eq_axiom(n, arg1, ~is_con);
         if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";