From 27ea23289ef39989c46da9a052a1ac41adede6d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Jan 2021 00:30:11 -0800 Subject: [PATCH] fix #4955 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_elim_eqs.cpp | 1 - src/sat/sat_scc.cpp | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index e8c6f6abd..928e84ebe 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -102,7 +102,6 @@ namespace sat { for (; it != end; ++it) { clause & c = *(*it); TRACE("sats", tout << "processing: " << c << "\n";); - TRACE("scc_details", m_solver.display_watches(tout);); unsigned sz = c.size(); unsigned i; for (i = 0; i < sz; i++) { diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp index 717a0cf44..e7adc33ec 100644 --- a/src/sat/sat_scc.cpp +++ b/src/sat/sat_scc.cpp @@ -220,7 +220,7 @@ namespace sat { frames.pop_back(); } } - TRACE("scc_details", m_solver.display_watches(tout);); + for (unsigned i = 0; i < m_solver.num_vars(); ++i) { if (roots[i] == null_literal) { roots[i] = literal(i, false);