From 76c9abada2405442e511d370b98bb7ad6ed353b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Aug 2015 11:00:19 -0700 Subject: [PATCH] remove dbg pp Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 6 +++++- src/tactic/core/simplify_tactic.cpp | 3 --- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 94917e190..1b4063b17 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -106,7 +106,11 @@ public: dep2asm_t dep2asm; VERIFY(l_true == internalize_formulas()); VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm)); - m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights); + svector nweights; + for (unsigned i = 0; i < m_asms.size(); ++i) { + nweights.push_back((unsigned) m_weights[i]); + } + m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr()); } lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 227a34b51..fea5ac86e 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -65,9 +65,6 @@ struct simplify_tactic::imp { proof * pr = g.pr(idx); new_pr = m().mk_modus_ponens(pr, new_pr); } - if (m_manager.is_false(new_curr)) { - std::cout << mk_pp(curr, m_manager) << " => " << new_curr << "\n"; - } g.update(idx, new_curr, new_pr, g.dep(idx)); } TRACE("after_simplifier_bug", g.display(tout););