From 63847be2c0121a75c45f4695e6d9c49a2b0c8b99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 14:40:41 +0200 Subject: [PATCH] Update theory_finite_set.cpp --- src/smt/theory_finite_set.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 28e2d95fc..c010278a1 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -43,14 +43,14 @@ namespace smt { internalize_term(atom); - // Track membership atoms (set.in) + // Track membership elements (set.in) expr* elem = nullptr, *set = nullptr; if (u.is_in(atom, elem, set)) { - auto n = get_enode(elem); - if (m_elements.contains(n)) - continue; - m_elements.insert(n); - ctx.trail().push(insert_obj_trail(n)); + auto n = ctx.get_enode(elem); + if (!m_elements.contains(n)) { + m_elements.insert(n); + ctx.push_trail(insert_obj_trail(n)); + } } return true;