From b5bf4be87eed877a04ebd87a730bbfec7ff0c211 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Mar 2026 15:40:45 -1000 Subject: [PATCH] fix: move m_fixed insertion after check_long_strings guard m_fixed.insert(e) was placed before the check_long_strings guard, causing check_fixed_length(false, false) to mark variables with len > 20 as processed without actually decomposing them. The subsequent check_fixed_length(false, true) then skipped them. Move the insertion after the guard so variables are only marked as fixed once they are actually decomposed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/theory_seq.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 38f67374e..34d30830f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -504,12 +504,6 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings m_fixed.contains(e)) { return false; } - - m_trail_stack.push(insert_obj_trail(m_fixed, e)); - m_fixed.insert(e); - - expr_ref seq(e, m), head(m), tail(m); - TRACE(seq, tout << "Fixed: " << mk_bounded_pp(e, m, 2) << " " << lo << "\n";); literal a = mk_eq(len_e, m_autil.mk_numeral(lo, true), false); @@ -519,6 +513,11 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero, bool check_long_strings if (!check_long_strings && lo > 20 && !is_zero) return false; + m_trail_stack.push(insert_obj_trail(m_fixed, e)); + m_fixed.insert(e); + + expr_ref seq(e, m), head(m), tail(m); + if (lo.is_zero()) { seq = m_util.str.mk_empty(e->get_sort()); }