mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

commented non-compiling debug traces

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-14 09:58:57 -08:00
parent 0b45828ff1
commit e45dc51e70
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_elim_vars.cpp
View file

@ -122,17 +122,17 @@ namespace sat{
bdd b = m.mk_exists(m_var2index[v], b0); bdd b = m.mk_exists(m_var2index[v], b0);
TRACE("elim_vars", TRACE("elim_vars",
tout << "eliminate " << v << "\n"; 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()) { if (w.is_binary_unblocked_clause()) {
tout << pos_l << " " << w.get_literal() << "\n"; tout << pos_l << " " << w.get_literal() << "\n";
} }
} }*/
m.display(tout, b1); 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()) { if (w.is_binary_unblocked_clause()) {
tout << neg_l << " " << w.get_literal() << "\n"; tout << neg_l << " " << w.get_literal() << "\n";
} }
} }*/
m.display(tout, b2); m.display(tout, b2);
clause_use_list::iterator itp = pos_occs.mk_iterator(); clause_use_list::iterator itp = pos_occs.mk_iterator();
while (!itp.at_end()) { while (!itp.at_end()) {