mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity

add a guard on m_fail

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-10 14:56:09 -07:00
parent a6d5c9762c
commit 5e54cb6693
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/levelwise.cpp
View file

@ -863,7 +863,7 @@ or
SASSERT(m_E.size() == 0); SASSERT(m_E.size() == 0);
apply_property_rules(prop_enum::_count); // reduce the level by one to be consumed by construct_interval apply_property_rules(prop_enum::_count); // reduce the level by one to be consumed by construct_interval
while (-- m_level > 0) while (-- m_level > 0)
if (!construct_interval()) if (m_fail || !construct_interval())
return std::vector<root_function_interval>(); // return empty return std::vector<root_function_interval>(); // return empty
return m_I; // the order of intervals is reversed return m_I; // the order of intervals is reversed