diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index a0adb6398..c81c7385a 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1383,7 +1383,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
             --i;
             tmp = args[i].get();
             tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp);
-            args[i] = tmp;
+            args[i] = std::move(tmp);
             sz += get_bv_size(to_app(arg)->get_arg(i));
         }
         result = m_autil.mk_add(args.size(), args.c_ptr());
@@ -2400,8 +2400,8 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) {
         return false;
     }
     unsigned sz = to_app(rhs)->get_num_args();
-    expr_ref t1(m()), t2(m());
-    t1 = to_app(rhs)->get_arg(0);
+    expr * t1 = to_app(rhs)->get_arg(0);
+    expr_ref t2(m());
     if (sz > 2) {
         t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1);
     }
@@ -2597,14 +2597,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
                 result = m().mk_bool_val(new_lhs == new_rhs);
                 return BR_DONE;
             }
-        }
-        else {
-            new_lhs = lhs;
-            new_rhs = rhs;
+            lhs = new_lhs;
+            rhs = new_rhs;
         }
 
-        lhs = new_lhs;
-        rhs = new_rhs;
         // Try to rewrite t1 + t2 = c --> t1 = c - t2
         // Reason: it is much cheaper to bit-blast.
         if (isolate_term(lhs, rhs, result)) {
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 4fbf77ec9..eb819c988 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -35,6 +35,7 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
 
+namespace {
 struct th_rewriter_cfg : public default_rewriter_cfg {
     bool_rewriter       m_b_rw;
     arith_rewriter      m_a_rw;
@@ -337,16 +338,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         family_id fid = t->get_family_id();
         if (fid == m_a_rw.get_fid()) {
             switch (t->get_decl_kind()) {
-            case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true;
-            case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
+            case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
             default:
                 return false;
             }
         }
         if (fid == m_bv_rw.get_fid()) {
             switch (t->get_decl_kind()) {
-            case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true;
-            case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true;
+            case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true;
             default:
                 return false;
             }
@@ -468,9 +469,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         // terms matched...
         bool is_int = m_a_util.is_int(t1);
         if (!new_t1)
-            new_t1 = m_a_util.mk_numeral(rational(0), is_int);
+            new_t1 = m_a_util.mk_numeral(rational::zero(), is_int);
         if (!new_t2)
-            new_t2 = m_a_util.mk_numeral(rational(0), is_int);
+            new_t2 = m_a_util.mk_numeral(rational::zero(), is_int);
         // mk common part
         ptr_buffer<expr> args;
         for (unsigned i = 0; i < num1; i++) {
@@ -709,6 +710,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
 
 };
+}
 
 template class rewriter_tpl<th_rewriter_cfg>;
 
@@ -764,8 +766,8 @@ unsigned th_rewriter::get_num_steps() const {
 
 void th_rewriter::cleanup() {
     ast_manager & m = m_imp->m();
-    dealloc(m_imp);
-    m_imp = alloc(imp, m, m_params);
+    m_imp->~imp();
+    new (m_imp) imp(m, m_params);
 }
 
 void th_rewriter::reset() {