From 6454e7fa3f541029868519c04acd16433ee2b33b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Feb 2023 11:03:04 -0800 Subject: [PATCH] apply rewriting if result of destructive equality resolution is simplified --- src/ast/rewriter/th_rewriter.cpp | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index c57d3aabc..93b867c45 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -821,17 +821,28 @@ struct th_rewriter_cfg : public default_rewriter_cfg { result_pr = m().mk_transitivity(p1, p2); } + TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;); + + proof_ref p2(m()); + expr_ref r(m()); + + bool der_change = false; if (is_quantifier(result)) { - proof_ref p2(m()); - expr_ref r(m()); m_der(to_quantifier(result), r, p2); + der_change = result.get() != r.get(); + if (m().proofs_enabled() && der_change) + result_pr = m().mk_transitivity(result_pr, p2); + result = r; + } + + if (der_change) { + th_rewriter rw(m()); + rw(result, r, p2); if (m().proofs_enabled() && result.get() != r.get()) result_pr = m().mk_transitivity(result_pr, p2); result = r; } - TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;); - SASSERT(old_q->get_sort() == result->get_sort()); return true; }