diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index 310269fec..123b496a1 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -24,8 +24,7 @@ Revision History:
 class ackermannize_bv_tactic : public tactic {
 public:
     ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
-        : m_m(m)
-        , m_p(p)
+        : m(m), m_p(p)
     {}
 
     virtual ~ackermannize_bv_tactic() { }
@@ -36,7 +35,6 @@ public:
         proof_converter_ref & pc,
         expr_dependency_ref & core) {
         mc = 0;
-        ast_manager& m(g->m());
         tactic_report report("ackermannize", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
@@ -44,11 +42,11 @@ public:
         expr_ref_vector flas(m);
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
-        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, NULL);
-        flas.reset();
+        lackr lackr(m, m_p, m_st, flas, NULL);
+
         // mk result
         goal_ref resg(alloc(goal, *g, true));
-        const bool success = imp->mk_ackermann(resg, m_lemma_limit);
+        const bool success = lackr.mk_ackermann(resg, m_lemma_limit);
         if (!success) { // Just pass on the input unchanged
             result.reset();
             result.push_back(g.get());
@@ -60,12 +58,12 @@ public:
         result.push_back(resg.get());
         // report model
         if (g->models_enabled()) {
-            mc = mk_ackermannize_bv_model_converter(m, imp->get_info());
+            mc = mk_ackermannize_bv_model_converter(m, lackr.get_info());
         }
 
-		resg->inc_depth();
-		TRACE("ackermannize", resg->display(tout););
-		SASSERT(resg->is_well_sorted());
+        resg->inc_depth();
+        TRACE("ackermannize", resg->display(tout););
+        SASSERT(resg->is_well_sorted());
     }
 
 
@@ -86,7 +84,7 @@ public:
         return alloc(ackermannize_bv_tactic, m, m_p);
     }
 private:
-    ast_manager&                         m_m;
+    ast_manager&                         m;
     params_ref                           m_p;
     lackr_stats                          m_st;
     double                               m_lemma_limit;
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index 1445ed611..411588d79 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -152,40 +152,7 @@ namespace smt {
         //      5) theory_arith fails to internalize (+ (* -1 x) (* -1 x)), and Z3 crashes.
         // 
 
-#if 0
-        // This block of code uses the simplifier for creating the literals t1 >= t2 and t1 <= t2.
-        // It has serious performance problems in VCC benchmarks.
-        // The problem seems to be the following:
-        // t1 and t2 are slacks (i.e., names for linear polynomials).
-        // The simplifier will create inequalities that will indirectly imply that t1 >= t2 and t1 <= t2.
-        // Example if: t1 := 1 + a
-        //             t2 := 2 + b
-        // the simplifier will create
-        // a - b >= -1
-        // a - b <= -1
-        // These inequalities imply that 1+a >= 2+b and 1+a <= 2+b,
-        // but the tableau is complete different.
-
-        
-        // BTW, note that we don't really need to handle the is_numeral case when using 
-        // the simplifier. However, doing that, it seems we minimize the performance problem.
-        expr_ref le(m);
-        expr_ref ge(m);
-        if (m_util.is_numeral(t1))
-            std::swap(t1, t2);
-        if (m_util.is_numeral(t2)) {
-            le = m_util.mk_le(t1, t2);
-            ge = m_util.mk_ge(t1, t2);
-        }
-        else {
-            arith_simplifier_plugin & s = *(get_simplifier());
-            s.mk_le(t1, t2, le);
-            s.mk_ge(t1, t2, ge);
-        }
-        TRACE("arith_eq_adapter_perf", tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
-#else
-        // Old version that used to be buggy.
-        // I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2 
+        // Requires that the theory arithmetic internalizer accept non simplified terms of the form t1 - t2 
         // if t1 and t2 already have slacks (theory variables) associated with them.
         // It also accepts terms with repeated variables (Issue #429).
         app * le = 0;
@@ -207,7 +174,6 @@ namespace smt {
         }
         TRACE("arith_eq_adapter_perf",
               tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
-#endif
 
         ctx.push_trail(already_processed_trail(m_already_processed, n1, n2));
         m_already_processed.insert(n1, n2, data(t1_eq_t2, le, ge));
diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h
index ac3035c78..7e9a645e6 100644
--- a/src/smt/arith_eq_adapter.h
+++ b/src/smt/arith_eq_adapter.h
@@ -65,7 +65,6 @@ namespace smt {
         theory &                         m_owner;
         theory_arith_params &            m_params;
         arith_util &                     m_util;
-        arith_simplifier_plugin *        m_as;
 
         already_processed                m_already_processed;
         enode_pair_vector                m_restart_pairs;
@@ -76,7 +75,7 @@ namespace smt {
         enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
 
     public:
-        arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {}
+        arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u) {}
         void new_eq_eh(theory_var v1, theory_var v2);
         void new_diseq_eh(theory_var v1, theory_var v2);
         void reset_eh();