mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

nits

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-30 08:37:32 -07:00
parent 661ccb3702
commit a73e244db4
2 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/substitution/substitution.cpp
View file

@ -301,10 +301,8 @@ bool substitution::acyclic(expr_offset p) {
bool substitution::acyclic() { bool substitution::acyclic() {
m_color.reset(); m_color.reset();
expr_offset r; expr_offset r;
svector<var_offset>::iterator it = m_vars.begin(); for (auto const& [k, v] : m_vars) {
svector<var_offset>::iterator end = m_vars.end(); m_subst.find(k, v, r);
for (; it != end; ++it) {
m_subst.find(it->first, it->second, r);
if (!acyclic(r)) if (!acyclic(r))
return false; return false;
} }