add obj_ref::operator=(obj_ref &&) + a few explicit uses

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) {

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);

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) {

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) {

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;