mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

We forgot relevant equations with one side being empty

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 10:40:33 +02:00
parent 684f93bed4
commit 803018b7c3
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1567,7 +1567,7 @@ namespace seq {
e->add_subst(subst);
child->apply_subst(m_sg, subst);
if (!lhs_rest->is_empty() && !rhs_rest->is_empty())
if (!lhs_rest->is_empty() || !rhs_rest->is_empty())
eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep));
return true;
}
@ -1602,7 +1602,7 @@ namespace seq {
e->add_subst(subst);
child->apply_subst(m_sg, subst);
if (!lhs_rest->is_empty() && !rhs_rest->is_empty())
if (!lhs_rest->is_empty() || !rhs_rest->is_empty())
eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep));
return true;
}