From 803018b7c3e3f1a9f3d8bd3ed72a11656d4df6ae Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 9 Apr 2026 10:40:33 +0200 Subject: [PATCH] We forgot relevant equations with one side being empty --- src/smt/seq/seq_nielsen.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 2cfd822a1..923a530a9 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -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; }