diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 894286a0262..1c374dcb84b 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2286,8 +2286,11 @@ br_status bv_rewriter::mk_mul_hoist(unsigned num_args, expr * const * args, expr
             unsigned sz = m_util.get_bv_size(z);
             ptr_vector<expr> new_args(num_args, args);
             rational p = rational(2).expt(sz) - 1;
-            new_args[i] = m_util.mk_bv_sub(mk_numeral(p, sz), z);
-            result = m_util.mk_bv_mul(num_args, new_args.data());
+            new_args[i] = mk_numeral(p, sz);
+            expr_ref a(m_util.mk_bv_mul(num_args, new_args.data()), m);
+            new_args[i] = z;
+            expr_ref b(m_util.mk_bv_mul(num_args, new_args.data()), m);
+            result = m_util.mk_bv_sub(a, b);
             return BR_REWRITE3;
         }
         // shl(z, u) * x = shl(x * z, u)
diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index d533ae1612f..521510b596c 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -21,7 +21,8 @@ Revision History:
 namespace smt {
     
     clause_proof::clause_proof(context& ctx):
-        ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m) {
+        ctx(ctx), m(ctx.get_manager()), m_lits(m), m_pp(m),
+        m_assumption(m), m_rup(m), m_del(m), m_smt(m) {
         
         auto proof_log = ctx.get_fparams().m_proof_log;
         m_has_log = proof_log.is_non_empty_string();
@@ -58,27 +59,35 @@ namespace smt {
         }
     }
 
-    proof* clause_proof::justification2proof(status st, justification* j) {
+    proof_ref clause_proof::justification2proof(status st, justification* j) {
         proof* r = nullptr;
         if (j)
             r = j->mk_proof(ctx.get_cr());
         if (r) 
-            return r;
+            return proof_ref(r, m);
         if (!is_enabled())
-            return nullptr;
+            return proof_ref(m);
         switch (st) {
         case status::assumption:
-            return m.mk_const("assumption", m.mk_proof_sort());
+            if (!m_assumption) 
+                m_assumption = m.mk_const("assumption", m.mk_proof_sort());
+            return m_assumption;
         case status::lemma:
-            return m.mk_const("rup", m.mk_proof_sort());
+            if (!m_rup)
+                m_rup = m.mk_const("rup", m.mk_proof_sort());
+            return m_rup;
         case status::th_lemma:
         case status::th_assumption:
-            return m.mk_const("smt", m.mk_proof_sort());
+            if (!m_smt)
+                m_smt = m.mk_const("smt", m.mk_proof_sort());
+            return m_smt;
         case status::deleted:
-            return m.mk_const("del", m.mk_proof_sort());
+            if (!m_del)
+                m_del = m.mk_const("del", m.mk_proof_sort());
+            return m_del;
         }
         UNREACHABLE();
-        return nullptr;
+        return proof_ref(m);
     }
 
     void clause_proof::add(clause& c) {
@@ -86,7 +95,7 @@ namespace smt {
             return;
         justification* j = c.get_justification();
         auto st = kind2st(c.get_kind());
-        proof_ref pr(justification2proof(st, j), m);
+        auto pr = justification2proof(st, j);
         CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
         update(c, st, pr);        
     }
@@ -95,7 +104,7 @@ namespace smt {
         if (!is_enabled())
             return;
         auto st = kind2st(k);
-        proof_ref pr(justification2proof(st, j), m);
+        auto pr = justification2proof(st, j);
         CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
         m_lits.reset();
         for (unsigned i = 0; i < n; ++i) 
@@ -110,7 +119,7 @@ namespace smt {
         m_lits.reset();
         for (unsigned i = 0; i < new_size; ++i) 
             m_lits.push_back(ctx.literal2expr(c[i]));
-        proof* p = justification2proof(status::lemma, nullptr);
+        auto p = justification2proof(status::lemma, nullptr);
         update(status::lemma, m_lits, p);
         for (unsigned i = new_size; i < c.get_num_literals(); ++i) 
             m_lits.push_back(ctx.literal2expr(c[i]));
@@ -124,7 +133,7 @@ namespace smt {
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit));
         auto st = kind2st(k);
-        proof* pr = justification2proof(st, j);
+        auto pr = justification2proof(st, j);
         update(st, m_lits, pr);
     }
 
@@ -135,7 +144,7 @@ namespace smt {
         m_lits.push_back(ctx.literal2expr(lit1));
         m_lits.push_back(ctx.literal2expr(lit2));
         auto st = kind2st(k);
-        proof* pr = justification2proof(st, j);
+        auto pr = justification2proof(st, j);
         update(st, m_lits, pr);
     }
 
diff --git a/src/smt/smt_clause_proof.h b/src/smt/smt_clause_proof.h
index b247a0454a3..1c593113669 100644
--- a/src/smt/smt_clause_proof.h
+++ b/src/smt/smt_clause_proof.h
@@ -63,13 +63,14 @@ namespace smt {
         void*                           m_on_clause_ctx = nullptr;
         ast_pp_util                     m_pp;
         scoped_ptr<std::ofstream>       m_pp_out;
+        proof_ref m_assumption, m_rup, m_del, m_smt;
 
         void init_pp_out();
         
         void update(status st, expr_ref_vector& v, proof* p);
         void update(clause& c, status st, proof* p);
         status kind2st(clause_kind k);
-        proof* justification2proof(status st, justification* j);
+        proof_ref justification2proof(status st, justification* j);
         void log(status st, proof* p);
         void declare(std::ostream& out, expr* e);
         std::ostream& display_literals(std::ostream& out, expr_ref_vector const& v);