From f352c250cf993890a424b511bdccdc03f267991c Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 15 Jun 2026 03:43:54 -0700 Subject: [PATCH] fix(seq::derive): re-apply intersect_intervals disjoint-case fix lost in rebase MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stage 2's revert commit (bcdbc80ab, Jun 14 18:06) restored intersect_intervals to the pre-fix shape that exists on master. The fb6470a1a fix on the derive branch (Jun 15 01:38) was authored AFTER that revert, so when derive-with-ranges was rebased onto the fixed derive branch the Stage 2 revert silently re-introduced the original bug: for (...) { if (hi < lo1 || lo > hi1) { j = old_sz; break; } // drops kept intervals if (hi1 >= lo) m_intervals[j++] = {...}; } On the regex-equivalence corpus this caused 514 false-unsat (master=sat, dwr=unsat) and 6 false-sat triangulated against master — matching the ~510 figure cited in fb6470a1a's commit message. Re-apply the canonical fix: drop only the disjoint interval and keep scanning. Verification (1523 files, -T:5, 8 workers): - Pre-fix dwr vs master: 514 SAT<->UNSAT disagreements (false-unsat 508). - Post-fix dwr vs master: 0 SAT<->UNSAT disagreements. - Post-fix dwr vs derive: 0 SAT<->UNSAT disagreements, 1 trivial sat->timeout diff. - 92/92 unit tests pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_derive.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 48db95e3b..d98885235 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -1252,21 +1252,18 @@ namespace seq { // Intersect the active suffix m_intervals[m_intervals_start..end] with [lo, hi] void derive::intersect_intervals(unsigned lo, unsigned hi) { // Copy active suffix to end, update start, then filter - unsigned old_start = m_intervals_start; unsigned old_sz = m_intervals.size(); - for (unsigned i = old_start; i < old_sz; ++i) + for (unsigned i = m_intervals_start; i < old_sz; ++i) m_intervals.push_back(m_intervals[i]); m_intervals_start = old_sz; - // Filter in-place within new suffix + // Filter in-place within new suffix: drop intervals disjoint from [lo,hi], + // keep the intersection for overlapping ones. unsigned j = m_intervals_start; for (unsigned i = m_intervals_start; i < m_intervals.size(); ++i) { auto [lo1, hi1] = m_intervals[i]; - if (hi < lo1 || lo > hi1) { - j = old_sz; - break; - } - if (hi1 >= lo) - m_intervals[j++] = {std::max(lo1, lo), std::min(hi1, hi)}; + if (hi < lo1 || lo > hi1) + continue; // disjoint with this interval — drop it + m_intervals[j++] = {std::max(lo1, lo), std::min(hi1, hi)}; } m_intervals.shrink(j); }