From 881d74278d822f229b8061b2b1710a57a81c1ad3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 17 Oct 2025 13:26:23 -0700 Subject: [PATCH] separate the lower and upper bound root functions Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index a5a29511e..a458d120a 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -402,9 +402,6 @@ namespace nlsat { std::sort(m_rel.m_rfunc.begin(), m_rel.m_rfunc.end(), [&](root_function const& a, root_function const& b){ return m_am.lt(a.val, b.val); }); - if (m_rel.m_rfunc.size() >= 2) { - enable_trace("lws"); - } TRACE(lws, if (m_rel.empty()) tout << "E is empty\n"; else { tout << "E:\n"; @@ -433,6 +430,11 @@ namespace nlsat { if (is_set(u)) for (unsigned j = u + 1; j < m_rel.m_rfunc.size(); j++) m_rel.add_pair(u, j); + + if (is_set(l) && is_set(u)) { + SASSERT(l + 1 == u); + m_rel.add_pair(l, u); + } } void fill_relation_pairs() {