From 776976cbd13f4627c4662cee43ecd5eba80a7210 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Feb 2026 20:21:51 -0800 Subject: [PATCH] fix #8572 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 5 ++++- src/ast/rewriter/seq_rewriter.cpp | 21 --------------------- 2 files changed, 4 insertions(+), 22 deletions(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 22114aecc..af6204de5 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -121,8 +121,11 @@ namespace seq { } expr_ref axioms::mk_len(expr* s) { - expr_ref result(seq.str.mk_length(s), m); + expr_ref len_s(seq.str.mk_length(s), m); + expr_ref result(len_s, m); m_rewrite(result); + if (result != len_s) + add_clause(mk_eq(len_s, result)); return result; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 962db6eb0..86bb297e9 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -561,29 +561,8 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { m_autil.is_numeral(z, r) && r >= 0) { expr* len_x = str().mk_length(x); result = m().mk_ite(m_autil.mk_le(len_x, z), len_x, z); - // expr* zero = m_autil.mk_int(0); - // result = m().mk_ite(m_autil.mk_le(z, zero), zero, result); return BR_REWRITE_FULL; } -#if 0 - expr* s = nullptr, *offset = nullptr, *length = nullptr; - if (str().is_extract(a, s, offset, length)) { - expr_ref len_s(str().mk_length(s), m()); - // if offset < 0 then 0 - // elif length <= 0 then 0 - // elif offset >= len(s) then 0 - // elif offset + length > len(s) then len(s) - offset - // else length - result = length; - result = m().mk_ite(m_autil.mk_gt(m_autil.mk_add(offset, length), len_s), - m_autil.mk_sub(len_s, offset), - result); - result = m().mk_ite(m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_le(length, zero()), m_autil.mk_lt(offset, zero())), - zero(), - result); - return BR_REWRITE_FULL; - } -#endif return BR_FAILED; }