From 2b31024dab127f8e685e20bf278ed54192d9a6ee Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Tue, 26 Jun 2018 17:00:56 +0100
Subject: [PATCH] add obj_ref::operator=(obj_ref &&) + a few explicit uses

---
 src/ast/rewriter/quant_hoist.cpp | 2 +-
 src/ast/rewriter/rewriter_def.h  | 2 +-
 src/ast/rewriter/th_rewriter.cpp | 2 +-
 src/qe/qe_lite.cpp               | 4 ++--
 src/util/obj_ref.h               | 9 +++++++++
 5 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index 3bd3cb3bc..b5cf57927 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -66,7 +66,7 @@ public:
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
-        fml = result;
+        fml = std::move(result);
     }
     
     void extract_quantifier(quantifier* q, app_ref_vector& vars, expr_ref& result, bool use_fresh) {
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 1a761e5d1..ebe52f52a 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -448,7 +448,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             m_r = result_stack().back();
             if (!is_ground(m_r)) {
                 m_inv_shifter(m_r, num_args, tmp);
-                m_r = tmp;
+                m_r = std::move(tmp);
             }
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(m_r);
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 0f4be71c9..4fbf77ec9 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -776,7 +776,7 @@ void th_rewriter::reset() {
 void th_rewriter::operator()(expr_ref & term) {
     expr_ref result(term.get_manager());
     m_imp->operator()(term, result);
-    term = result;
+    term = std::move(result);
 }
 
 void th_rewriter::operator()(expr * t, expr_ref & result) {
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 494773f5d..3223706d4 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2297,14 +2297,14 @@ public:
             vars.resize(j);
         }
         else {
-            fml = tmp;
+            fml = std::move(tmp);
         }
     }
 
     void operator()(expr_ref& fml, proof_ref& pr) {
         expr_ref tmp(m);
         m_elim_star(fml, tmp, pr);
-        fml = tmp;
+        fml = std::move(tmp);
     }
 
     void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h
index 409a77fc0..885601375 100644
--- a/src/util/obj_ref.h
+++ b/src/util/obj_ref.h
@@ -92,6 +92,15 @@ public:
         return *this;
     }
 
+    obj_ref & operator=(obj_ref && n) {
+        SASSERT(&m_manager == &n.m_manager);
+        if (this != &n) {
+            std::swap(m_obj, n.m_obj);
+            n.reset();
+        }
+        return *this;
+    }
+
     void reset() {
         dec_ref();
         m_obj = nullptr;