From 1a584a216499e744b43f8cce3f5ab7340ea4028d Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 7 Jul 2026 16:07:19 -0700 Subject: [PATCH] Remove pointless generation assignment for eq atom --- src/smt/smt_context.cpp | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f647cab383..ffc6155625 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; } }