mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

fix bug in intersection iterator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-04 16:26:51 -07:00
parent 3a4cdfdc26
commit 3f62cb9932
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_split.cpp
View file

@ -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 {