mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

fix(seq::derive): re-apply intersect_intervals disjoint-case fix lost in rebase

Browse source 
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>
This commit is contained in:
Margus Veanes 2026-06-15 03:43:54 -07:00
parent c0c826cf5f
commit f352c250cf
1 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/seq_derive.cpp
View file

@ -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);
}