mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-16 03:55:42 +00:00
Code Activity

fixing unsoundness in concat rule

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 12:24:06 -07:00
parent 3abdf5928a
commit b095adfa81
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,7 +36,6 @@ struct split_set::imp {
if (r) {
VERIFY(seq.is_re(r, m_seq_sort));
m_re_sort = r->get_sort();
TRACE(seq, tout << "split_set::imp: " << this << " " << mk_pp(r, m) << " threshold: " << m_threshold << "\n");
}
if (m_threshold == 0)
m_threshold = UINT_MAX;
@ -453,7 +452,6 @@ struct split_set::iterator::imp {
}
bool at_end() const {
TRACE(seq, tout << "split_set::iterator::at_end: " << this << " " << m_at_end << " " << m_qhead << "/" << m_splits.size() << "\n");
return m_failure || (m_at_end && m_qhead == m_splits.size());
}
};