diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp
index 027846c31..c95c07f63 100644
--- a/src/ast/rewriter/der.cpp
+++ b/src/ast/rewriter/der.cpp
@@ -374,13 +374,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
     expr_ref_buffer  new_patterns(m_manager);
     expr_ref_buffer  new_no_patterns(m_manager);
     for (unsigned j = 0; j < q->get_num_patterns(); j++) {
-        expr_ref new_pat = m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr());
-        new_patterns.push_back(new_pat);
+        new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
     }
 
     for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
-        expr_ref new_nopat = m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr());
-        new_no_patterns.push_back(new_nopat);
+        new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
     }
 
     r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
diff --git a/src/ast/rewriter/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp
index 54d7e2eca..c621579cb 100644
--- a/src/ast/rewriter/distribute_forall.cpp
+++ b/src/ast/rewriter/distribute_forall.cpp
@@ -126,8 +126,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
             br.mk_not(arg, not_arg);
             quantifier_ref tmp_q(m_manager);
             tmp_q = m_manager.update_quantifier(q, not_arg);
-            expr_ref new_q = elim_unused_vars(m_manager, tmp_q, params_ref());
-            new_args.push_back(new_q);
+            new_args.push_back(elim_unused_vars(m_manager, tmp_q, params_ref()));
         }
         expr_ref result(m_manager);
         // m_bsimp.mk_and actually constructs a (not (or ...)) formula,
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index cbd79e08c..ff479b565 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -135,17 +135,14 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
         return result;
     }
 
-    expr_ref tmp(m);
     expr_ref_buffer new_patterns(m);
     expr_ref_buffer new_no_patterns(m);
 
     for (unsigned i = 0; i < num_patterns; i++) {
-        tmp = m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr());
-        new_patterns.push_back(tmp);
+        new_patterns.push_back(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
     }
     for (unsigned i = 0; i < num_no_patterns; i++) {
-        tmp = m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr());
-        new_no_patterns.push_back(tmp);
+        new_no_patterns.push_back(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
     }
 
     result = m.mk_quantifier(q->get_kind(),
diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp
index c2688f741..800644d9e 100644
--- a/src/tactic/core/distribute_forall_tactic.cpp
+++ b/src/tactic/core/distribute_forall_tactic.cpp
@@ -49,8 +49,7 @@ class distribute_forall_tactic : public tactic {
                     expr * not_arg = m.mk_not(arg);
                     quantifier_ref tmp_q(m);
                     tmp_q = m.update_quantifier(old_q, not_arg);
-                    expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref());
-                    new_args.push_back(new_q);
+                    new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
                 }
                 result = m.mk_and(new_args.size(), new_args.c_ptr());
                 return true;
@@ -68,8 +67,7 @@ class distribute_forall_tactic : public tactic {
                     expr * arg     = to_app(new_body)->get_arg(i);
                     quantifier_ref tmp_q(m);
                     tmp_q = m.update_quantifier(old_q, arg);
-                    expr_ref new_q = elim_unused_vars(m, tmp_q, params_ref());
-                    new_args.push_back(new_q);
+                    new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));
                 }
                 result = m.mk_and(new_args.size(), new_args.c_ptr());
                 return true;