mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-07 23:05:06 +00:00
Code Activity

Update theory_finite_set.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-15 14:40:41 +02:00 • committed by GitHub
parent 9b7967dacf
commit 63847be2c0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_finite_set.cpp
View file

@ -43,14 +43,14 @@ namespace smt {
internalize_term(atom); internalize_term(atom);
// Track membership atoms (set.in) // Track membership elements (set.in)
expr* elem = nullptr, *set = nullptr; expr* elem = nullptr, *set = nullptr;
if (u.is_in(atom, elem, set)) { if (u.is_in(atom, elem, set)) {
auto n = get_enode(elem); auto n = ctx.get_enode(elem);
if (m_elements.contains(n)) if (!m_elements.contains(n)) {
continue; m_elements.insert(n);
m_elements.insert(n); ctx.push_trail(insert_obj_trail(n));
ctx.trail().push(insert_obj_trail(n)); }
} }
return true; return true;