From 3f62cb9932dfbf84222a5dcbfe96a409b1d56016 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Jul 2026 16:26:51 -0700 Subject: [PATCH] fix bug in intersection iterator Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_split.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index c1b1b6463d..394edfb334 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -67,17 +67,19 @@ struct split_set::iterator::imp { a_it(a_s.begin()), a_end(a_s.end()), b_it(b_s.begin()), b_end(b_s.end()) {} bool at_end() const { - return (a_it == a_end && b_it == b_end) || a_it.failed() || b_it.failed(); + return b_it == b_end || a_it == a_end || a_it.failed() || b_it.failed(); } void next() { SASSERT(!at_end()); - if (b_it != b_end) - ++b_it; + SASSERT(b_it != b_end); + ++b_it; if (b_it == b_end) { ++a_it; - if (a_it != a_end) + if (a_it != a_end) { b_it.m_imp->rewind(); + SASSERT(b_it != b_end); + } } } void consume() override {