mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Added debug traces.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-09 16:36:49 +01:00
parent ff3c630207
commit f54a7db108
2 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/tactic/smt_tactic.cpp
View file

@ -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);

1
src/solver/solver_na2as.cpp
View file

@ -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());
}