mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity

relax an assert

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-18 14:44:23 -07:00
parent c2661e34fc
commit 0baaa3f9ce
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -1019,14 +1019,14 @@ or
init_properties(); // initializes m_Q as a queue of properties on levels <= m_n init_properties(); // initializes m_Q as a queue of properties on levels <= m_n
SASSERT(m_rel.empty()); 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 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); SASSERT(m_level == m_n);
do { // m_level changes from m_n - 1 to 0 do { // m_level changes from m_n - 1 to 0
m_level--; m_level--;
if (m_fail || !construct_interval()) if (m_fail || !construct_interval())
return std::vector<root_function_interval>(); // return empty return std::vector<root_function_interval>(); // return empty
} while (m_level != 0); } while (m_level != 0);
return m_I; // the order of intervals is reversed return m_I;
} }
// Pretty-print helpers // Pretty-print helpers