From 7922ee3e82731fa34dfbf35cdd0323b73ead44a3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 20 Mar 2024 15:37:34 +0100 Subject: [PATCH] debug output --- src/sat/smt/polysat/project_interval.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat/project_interval.cpp b/src/sat/smt/polysat/project_interval.cpp index 635cdff75..27e10f5d5 100644 --- a/src/sat/smt/polysat/project_interval.cpp +++ b/src/sat/smt/polysat/project_interval.cpp @@ -67,8 +67,10 @@ namespace polysat { return; } 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); + 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 { if (f.child == null_var) 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) {