mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-04 16:10:50 +00:00
Code Activity

Update used_enodes properly (#9695)

Browse source 
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 <t-cancebeci@microsoft.com>
This commit is contained in:
Can Cebeci 2026-06-03 13:36:37 -07:00 • committed by GitHub
parent d64ce41b2e
commit 14746d7fb6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/mam.cpp
View file

@ -1881,8 +1881,10 @@ namespace {
m_pool.recycle(v); m_pool.recycle(v);
} }
void update_max_generation(enode * n, enode * prev) { void update_max_generation(enode * n, enode * prev, enode * min_gen_match=nullptr) {
m_max_generation = std::max(m_max_generation, n->get_generation()); 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)) if (m.has_trace_stream() || is_trace_enabled(TraceTag::causality))
m_used_enodes.push_back(std::make_tuple(prev, n)); m_used_enodes.push_back(std::make_tuple(prev, n));
@ -1910,15 +1912,18 @@ namespace {
} }
while (curr != first); while (curr != first);
if (matching_cgr) if (matching_cgr)
update_max_generation(min_gen_match, first); update_max_generation(matching_cgr, first, min_gen_match);
return matching_cgr; return matching_cgr;
} }
enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) { enode * get_next_f_app(func_decl * lbl, unsigned num_expected_args, enode * first, enode * curr) {
curr = curr->get_next(); curr = curr->get_next();
while (curr != first) { 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; return curr;
}
curr = curr->get_next(); curr = curr->get_next();
} }
return nullptr; return nullptr;