From 82a89120b09625c77742046b5817eac4e754ef9f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Dec 2018 15:26:40 -0800 Subject: [PATCH] fix #2042 Signed-off-by: Nikolaj Bjorner --- src/ast/pattern/pattern_inference.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index cf3c8bc31..93b269f87 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -594,7 +594,6 @@ bool pattern_inference_cfg::reduce_quantifier( unsigned new_weight; if (m_database.match_quantifier(q, new_patterns, new_weight)) { DEBUG_CODE(for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); }); - quantifier_ref new_q(m); if (q->get_num_patterns() > 0) { // just update the weight... TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";); @@ -604,10 +603,10 @@ bool pattern_inference_cfg::reduce_quantifier( quantifier_ref tmp(m); tmp = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr()); result = m.update_quantifier_weight(tmp, new_weight); - TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";); + TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(result, m) << "\n";); } if (m.proofs_enabled()) - result_pr = m.mk_rewrite(q, new_q); + result_pr = m.mk_rewrite(q, result); return true; } }