From e45dc51e70dea7c6b754f5faedf243763da5631e Mon Sep 17 00:00:00 2001 From: Miguel Angelo Da Terra Neves Date: Thu, 14 Dec 2017 09:58:57 -0800 Subject: [PATCH] commented non-compiling debug traces Signed-off-by: Miguel Angelo Da Terra Neves --- src/sat/sat_elim_vars.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 379888b15..f9f06f222 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -122,17 +122,17 @@ namespace sat{ bdd b = m.mk_exists(m_var2index[v], b0); TRACE("elim_vars", tout << "eliminate " << v << "\n"; - for (watched const& w : simp.get_wlist(~pos_l)) { + /*for (watched const& w : simp.get_wlist(~pos_l)) { if (w.is_binary_unblocked_clause()) { tout << pos_l << " " << w.get_literal() << "\n"; } - } + }*/ m.display(tout, b1); - for (watched const& w : simp.get_wlist(~neg_l)) { + /*for (watched const& w : simp.get_wlist(~neg_l)) { if (w.is_binary_unblocked_clause()) { tout << neg_l << " " << w.get_literal() << "\n"; } - } + }*/ m.display(tout, b2); clause_use_list::iterator itp = pos_occs.mk_iterator(); while (!itp.at_end()) {