From 14746d7fb6d844e5c6e1a0c95dd5b3e4f5a7c83c Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Wed, 3 Jun 2026 13:36:37 -0700 Subject: [PATCH] Update used_enodes properly (#9695) https://github.com/Z3Prover/z3/pull/9405 made the trace report used_enodes incorrectly, since the previous code relied on update_max_generation to maintain the relevant data structure. This should fix it. Co-authored-by: Can Cebeci --- src/smt/mam.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index db2ddc4ca..80918fcb4 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1881,8 +1881,10 @@ namespace { m_pool.recycle(v); } - void update_max_generation(enode * n, enode * prev) { - m_max_generation = std::max(m_max_generation, n->get_generation()); + void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) { + unsigned new_gen = min_gen_match ? min_gen_match->get_generation() : n->get_generation(); + + m_max_generation = std::max(m_max_generation, new_gen); if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) m_used_enodes.push_back(std::make_tuple(prev, n)); @@ -1910,15 +1912,18 @@ namespace { } while (curr != first); if (matching_cgr) - update_max_generation(min_gen_match, first); + update_max_generation(matching_cgr, first, min_gen_match); return matching_cgr; } enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) { curr = curr->get_next(); while (curr != first) { - if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) + if (curr->get_decl() == lbl && curr->get_num_args() == num_expected_args && curr->is_cgr()) { + if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality)) + m_used_enodes.push_back(std::make_tuple(first, curr)); return curr; + } curr = curr->get_next(); } return nullptr;