From 0baaa3f9cedc893f33ae0120b651d79065ff6e5e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 18 Oct 2025 14:44:23 -0700 Subject: [PATCH] relax an assert Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 6cc86a329..4c4121d8c 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1019,14 +1019,14 @@ or init_properties(); // initializes m_Q as a queue of properties on levels <= m_n SASSERT(m_rel.empty()); apply_property_rules(prop_enum::_count); // reduce the level from m_n to m_n - 1 to be consumed by construct_interval - SASSERT(m_Q[m_n].size() == 0); + SASSERT(m_Q[m_n].size() == 0 || m_fail); SASSERT(m_level == m_n); do { // m_level changes from m_n - 1 to 0 m_level--; if (m_fail || !construct_interval()) return std::vector(); // return empty } while (m_level != 0); - return m_I; // the order of intervals is reversed + return m_I; } // Pretty-print helpers