diff --git a/src/ast/euf/euf_seq_plugin.cpp b/src/ast/euf/euf_seq_plugin.cpp index 422d1d2b2..9173c9c10 100644 --- a/src/ast/euf/euf_seq_plugin.cpp +++ b/src/ast/euf/euf_seq_plugin.cpp @@ -159,9 +159,11 @@ namespace euf { return; enode* existing = nullptr; - if (m_concat_table.find(n, existing) && existing != n) - push_merge(n, existing); - else if (!existing) { + if (m_concat_table.find(n, existing)) { + if (existing != n) + push_merge(n, existing); + } + else { m_concat_table.insert(n); m_concats.push_back(n); push_undo(undo_kind::undo_add_to_table);