From f54a7db1086b8151d42315ae7e2d96efa8ebdbd0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 9 Aug 2016 16:36:49 +0100 Subject: [PATCH] Added debug traces. --- src/smt/tactic/smt_tactic.cpp | 1 + src/solver/solver_na2as.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index baaaf7bb0..f2fbcf6d9 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -199,6 +199,7 @@ public: tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; tout << "params_ref: " << m_params_ref << "\n"; tout << "nnf: " << fparams().m_nnf_cnf << "\n";); + TRACE("smt_tactic_params", m_params.display(tout);); TRACE("smt_tactic_detail", in->display(tout);); TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); scoped_init_ctx init(*this, m); diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 99917fff8..29ce4864f 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -62,6 +62,7 @@ struct append_assumptions { lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) { append_assumptions app(m_assumptions, num_assumptions, assumptions); + TRACE("solver_na2as", display(tout);); return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr()); }