Merge branch 'master' of https://github.com/z3prover/z3

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

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);
-        dealloc(m_imp);
-        m_imp = nullptr;
-    }
     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;

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(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
-        new_patterns.push_back(new_pat);
     }
 
     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(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr()));
-        new_no_patterns.push_back(new_nopat);
     }
 
     r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),

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(elim_unused_vars(m_manager, tmp_q, params_ref()));
-            new_args.push_back(new_q);
         }
         expr_ref result(m_manager);
         // m_bsimp.mk_and actually constructs a (not (or ...)) formula,

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(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
-        new_patterns.push_back(tmp);
     }
     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(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr()));
-        new_no_patterns.push_back(tmp);
     }
 
     result = m.mk_quantifier(q->get_kind(),

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -37,7 +37,6 @@ class elim_small_bv_tactic : public tactic {
         bv_util                     m_util;
         th_rewriter                 m_simp;
         ref<generic_model_converter> m_mc;
-        goal *                      m_goal;
         unsigned                    m_max_bits;
         unsigned long long          m_max_steps;
         unsigned long long          m_max_memory; // in bytes
@@ -53,7 +52,6 @@ class elim_small_bv_tactic : public tactic {
             m_bindings(_m),
             m_num_eliminated(0) {
             updt_params(p);
-            m_goal = nullptr;
             m_max_steps = UINT_MAX;
         }
 
@@ -76,7 +74,7 @@ class elim_small_bv_tactic : public tactic {
             TRACE("elim_small_bv", tout << "replace idx " << idx << " with " << mk_ismt2_pp(replacement, m) <<
                 " in " << mk_ismt2_pp(e, m) << std::endl;);
             expr_ref res(m);
-            expr_ref_vector substitution(m);
+            ptr_vector<expr> substitution;
 
             substitution.resize(num_decls, nullptr);
             substitution[num_decls - idx - 1] = replacement;
@@ -94,7 +92,7 @@ class elim_small_bv_tactic : public tactic {
 
             TRACE("elim_small_bv", tout << "substitution: " << std::endl;
                                     for (unsigned k = 0; k < substitution.size(); k++) {
-                                        expr * se = substitution[k].get();
+                                        expr * se = substitution[k];
                                         tout << k << " = ";
                                         if (se == 0) tout << "0";
                                         else tout << mk_ismt2_pp(se, m);
@@ -152,9 +150,7 @@ class elim_small_bv_tactic : public tactic {
                     expr_ref_vector new_bodies(m);
                     for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) {
                         expr_ref n(m_util.mk_numeral(j, bv_sz), m);
-                        expr_ref nb(m);
+                        new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n));
-                        nb = replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n);
-                        new_bodies.push_back(nb);
                         num_steps++;
                     }
 
@@ -250,7 +246,6 @@ public:
         fail_if_unsat_core_generation("elim-small-bv", g);
         m_rw.cfg().m_produce_models = g->models_enabled();
 
-        m_rw.m_cfg.m_goal = g.get();
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
         unsigned   size = g->size();

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(elim_unused_vars(m, tmp_q, params_ref()));
-                    new_args.push_back(new_q);
                 }
                 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(elim_unused_vars(m, tmp_q, params_ref()));
-                    new_args.push_back(new_q);
                 }
                 result = m.mk_and(new_args.size(), new_args.c_ptr());
                 return true;

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);
-            std::swap(m_obj, n.m_obj);
+        n.reset();
-            n.reset();
-        }
         return *this;
     }
 

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

src/util/ref_vector.h

@@ -99,8 +99,8 @@ public:
         return *this;
     }
 
-    template <typename W, typename M>
+    template <typename M>
-    ref_vector_core& push_back(obj_ref<W,M> && n) {
+    ref_vector_core& push_back(obj_ref<T,M> && n) {
         m_nodes.push_back(n.get());
         n.steal();
         return *this;