mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-14 21:05:39 +00:00
Code Activity

remove warnings

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-02 16:45:01 -10:00
parent 4587ecec9c
commit 156a7da4d1
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/levelwise.cpp
View file

@ -672,7 +672,7 @@ namespace nlsat {
for (unsigned i = 1; i < both.size(); ++i) for (unsigned i = 1; i < both.size(); ++i)
if (both[i].upper_rf < both[upper_root_idx].upper_rf) if (both[i].upper_rf < both[upper_root_idx].upper_rf)
upper_root_idx = i; upper_root_idx = i;
unsigned lower_root_idx = both.size() - 1; (void)upper_root_idx; // used in DEBUG_CODE below
// Process in order of lower_rf // Process in order of lower_rf
// First element (index 0) has min lower_rf // First element (index 0) has min lower_rf
@ -693,7 +693,9 @@ namespace nlsat {
} }
// Check arborescence invariants // Check arborescence invariants (used in debug via SASSERT)
DEBUG_CODE(
unsigned lower_root_idx = both.size() - 1;
auto arb_invariant = [&]() { auto arb_invariant = [&]() {
// Reconstruct parent[] from the algorithm logic // Reconstruct parent[] from the algorithm logic
std_vector<unsigned> parent(both.size(), UINT_MAX); std_vector<unsigned> parent(both.size(), UINT_MAX);
@ -780,7 +782,7 @@ namespace nlsat {
return true; return true;
}; };
SASSERT(arb_invariant()); SASSERT(arb_invariant()););
} }
// Sector spanning tree heuristic: // Sector spanning tree heuristic: