mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Remove pointless generation assignment for eq atom

Browse source
This commit is contained in:
Can Cebeci 2026-07-07 16:07:19 -07:00
parent 0a8e7e2842
commit 1a584a2164
1 changed files with 1 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -680,14 +680,9 @@ namespace smt {
m_dyn_ack_manager.cg_conflict_eh(n1->get_app(), n2->get_app());
assign(literal(v), mk_justification(eq_propagation_justification(lhs, rhs)));
}
if (parent->is_cgc_enabled()) {
auto [p, parent_generation] = m_r1_parent_generations[cgc_enabled_idx++];
SASSERT(p == parent);
parent->m_generation = parent_generation;
}
// It is not necessary to reinsert the equality to the congruence table
// (because the only congruence propagations that could lead to are already handled by the assign() here).
continue;
}
}