mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

debug output

Browse source
This commit is contained in:
Jakob Rath 2024-03-20 15:37:34 +01:00
parent fd9c931168
commit 7922ee3e82
1 changed files with 7 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/polysat/project_interval.cpp
View file

@ -67,8 +67,10 @@ namespace polysat {
return; return;
} }
for (auto const& f : m_fixed) { for (auto const& f : m_fixed) {
unsigned level = c.level(dep_fixed(f)); dependency dep = dep_fixed(f);
unsigned level = c.level(dep);
m_fixed_levels.push_back(level); m_fixed_levels.push_back(level);
IF_VERBOSE(4, verbose_stream() << "dep_fixed " << dep << " at level " << level << "\n");
} }
} }
@ -92,7 +94,10 @@ namespace polysat {
auto compute_target_level = [&](fixed_slice const& f) -> unsigned { auto compute_target_level = [&](fixed_slice const& f) -> unsigned {
if (f.child == null_var) if (f.child == null_var)
return UINT_MAX; return UINT_MAX;
return c.level(dep_target(f)); dependency dep = dep_target(f);
unsigned level = c.level(dep);
IF_VERBOSE(4, verbose_stream() << "dep_target " << dep << " at level " << level << "\n");
return level;
}; };
for (auto const& f : m_fixed) { for (auto const& f : m_fixed) {