From edf0df634d5564cff49b463851081f5a135261f2 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Tue, 19 Feb 2019 13:18:20 +0000
Subject: [PATCH] simplifications to refs

---
 src/ackermannization/lackr.cpp                   |  2 +-
 src/ackermannization/lackr_model_constructor.cpp | 10 +++-------
 src/util/obj_ref.h                               |  6 ++----
 src/util/ref_buffer.h                            |  6 ++++++
 src/util/ref_vector.h                            |  4 ++--
 5 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index a965fc261..4fe7797d4 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -122,7 +122,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
     TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
     if (m_m.is_true(cga)) return false;
     m_st.m_ackrs_sz++;
-    m_ackrs.push_back(cga);
+    m_ackrs.push_back(std::move(cga));
     return true;
 }
 
diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp
index df0aac15e..f24a53cdb 100644
--- a/src/ackermannization/lackr_model_constructor.cpp
+++ b/src/ackermannization/lackr_model_constructor.cpp
@@ -237,7 +237,7 @@ struct lackr_model_constructor::imp {
             // handle functions
             if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted
                 app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m);
-                if (!make_value_uninterpreted_function(a, values, key.get(), result)) {
+                if (!make_value_uninterpreted_function(a, key.get(), result)) {
                     return false;
                 }
             }
@@ -284,7 +284,6 @@ struct lackr_model_constructor::imp {
         }
 
         bool make_value_uninterpreted_function(app* a,
-                expr_ref_vector& values,
                 app* key,
                 expr_ref& result) {
             // get ackermann constant
@@ -370,15 +369,12 @@ lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref i
 {}
 
 lackr_model_constructor::~lackr_model_constructor() {
-    if (m_imp) dealloc(m_imp);
+    dealloc(m_imp);
 }
 
 bool lackr_model_constructor::check(model_ref& abstr_model) {
     m_conflicts.reset();
-    if (m_imp) {
-        dealloc(m_imp);
-        m_imp = nullptr;
-    }
+    dealloc(m_imp);
     m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts);
     const bool rv = m_imp->check();
     m_state = rv ? CHECKED : CONFLICT;
diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h
index 8908f2cdd..e3b0d0710 100644
--- a/src/util/obj_ref.h
+++ b/src/util/obj_ref.h
@@ -94,10 +94,8 @@ public:
 
     obj_ref & operator=(obj_ref && n) {
         SASSERT(&m_manager == &n.m_manager);
-        if (this != &n) {
-            std::swap(m_obj, n.m_obj);
-            n.reset();
-        }
+        std::swap(m_obj, n.m_obj);
+        n.reset();
         return *this;
     }
 
diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h
index 4768c3f28..49213cc62 100644
--- a/src/util/ref_buffer.h
+++ b/src/util/ref_buffer.h
@@ -58,6 +58,12 @@ public:
         inc_ref(n);
         m_buffer.push_back(n);
     }
+
+    template <typename M>
+    void push_back(obj_ref<T,M> && n) {
+        m_buffer.push_back(n.get());
+        n.steal();
+    }
     
     void pop_back() {
         SASSERT(!m_buffer.empty());
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index d0e9a8f55..732ec20dd 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -99,8 +99,8 @@ public:
         return *this;
     }
 
-    template <typename W, typename M>
-    ref_vector_core& push_back(obj_ref<W,M> && n) {
+    template <typename M>
+    ref_vector_core& push_back(obj_ref<T,M> && n) {
         m_nodes.push_back(n.get());
         n.steal();
         return *this;