From e0a71cd2b41b223216cb9d8e0df7cf86c2e4e57c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 20 Dec 2025 06:52:34 -1000 Subject: [PATCH] index bug Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 160845035..39916ccde 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -375,7 +375,7 @@ namespace nlsat { std::sort(rfs.begin(), mid, cmp); std::sort(mid, rfs.end(), cmp); 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)); if (mid != rfs.begin()) { auto& r = *(mid - 1); @@ -394,6 +394,7 @@ namespace nlsat { } } else { // mid == rfs.begin() auto & r = *mid; + u_index = 0; I.u = r.ire.p; I.u_index = r.ire.i; }