mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-03 20:24:36 +00:00
Code Activity

index bug

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-20 06:52:34 -10:00
parent 5166d9111b
commit e0a71cd2b4
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/levelwise.cpp
View file

@ -375,7 +375,7 @@ namespace nlsat {
std::sort(rfs.begin(), mid, cmp); std::sort(rfs.begin(), mid, cmp);
std::sort(mid, rfs.end(), cmp); std::sort(mid, rfs.end(), cmp);
auto & I = m_I[m_level]; auto & I = m_I[m_level];
unsigned l_index = -1, u_index = -1; unsigned l_index = -1, u_index = -1; // indices in rfs
SASSERT(mid == rfs.end() || m_am.lt(v, mid->val)); SASSERT(mid == rfs.end() || m_am.lt(v, mid->val));
if (mid != rfs.begin()) { if (mid != rfs.begin()) {
auto& r = *(mid - 1); auto& r = *(mid - 1);
@ -394,6 +394,7 @@ namespace nlsat {
} }
} else { // mid == rfs.begin() } else { // mid == rfs.begin()
auto & r = *mid; auto & r = *mid;
u_index = 0;
I.u = r.ire.p; I.u_index = r.ire.i; I.u = r.ire.p; I.u_index = r.ire.i;
} }