inherit weights

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/ast/ast.cpp

@@ -401,7 +401,7 @@ quantifier::quantifier(unsigned num_decls, sort * const * decl_sorts, symbol con
     m_expr(body),
     m_sort(s),
     m_depth(::get_depth(body) + 1),
-    m_weight(0),
+    m_weight(1),
     m_has_unused_vars(true),
     m_has_labels(::has_labels(body)),
     m_qid(symbol()),

src/tactic/arith/purify_arith_tactic.cpp

@@ -740,7 +740,7 @@ struct purify_arith_proc {
             scoped_ptr<expr_replacer> replacer = mk_default_expr_replacer(m());
             replacer->set_substitution(&subst);
             (*replacer)(new_body, new_body);
-            new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body);
+            new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight());
             result = m().update_quantifier(q, new_body);
             if (m_produce_proofs) {
                 proof_ref_vector & cnstr_prs = r.cfg().m_new_cnstr_prs;

src/tactic/core/reduce_invertible_tactic.cpp

@@ -469,7 +469,7 @@ class reduce_invertible_tactic : public tactic {
             }
             if (has_new_var) {
                 sub(new_body, result);
-                result = m.mk_quantifier(old_q->get_kind(), new_sorts.size(), new_sorts.c_ptr(), old_q->get_decl_names(), result);
+                result = m.mk_quantifier(old_q->get_kind(), new_sorts.size(), new_sorts.c_ptr(), old_q->get_decl_names(), result, old_q->get_weight());
                 result_pr = nullptr;
                 return true;
             }