From b1bae695e68e66cc847cc9f0df07eb5257767b4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Mar 2026 16:32:01 -0700 Subject: [PATCH] comment Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 9e1335cb2..cb2fac901 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -223,6 +223,7 @@ namespace seq { return false; } + // NSB review: optimize sg.subst to apply join only if the substitution had an effect. void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { if (!s.m_var) return; for (unsigned i = 0; i < m_str_eq.size(); ++i) {