mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-01 06:37:49 +00:00
Code Activity

comment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-17 16:32:01 -07:00
parent 2847dd8bb3
commit b1bae695e6
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/seq/seq_nielsen.cpp
View file

@ -223,6 +223,7 @@ namespace seq {
return false; 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) { void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
if (!s.m_var) return; if (!s.m_var) return;
for (unsigned i = 0; i < m_str_eq.size(); ++i) { for (unsigned i = 0; i < m_str_eq.size(); ++i) {