mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

dbg printing

Browse source
This commit is contained in:
Mikolas Janota 2016-01-27 16:27:31 +00:00
parent 4b37140780
commit e318d460d7
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/ackr/lackr.cpp
View file

@ -124,6 +124,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
// Introduce the ackermann lemma for each pair of terms. // Introduce the ackermann lemma for each pair of terms.
// //
void lackr::eager_enc() { void lackr::eager_enc() {
TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;);
const fun2terms_map::iterator e = m_fun2terms.end(); const fun2terms_map::iterator e = m_fun2terms.end();
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) { for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
checkpoint(); checkpoint();
@ -262,6 +263,7 @@ void lackr::collect_terms() {
expr_mark visited; expr_mark visited;
for(unsigned i = 0; i < m_formulas.size(); ++i) { for(unsigned i = 0; i < m_formulas.size(); ++i) {
stack.push_back(m_formulas.get(i)); stack.push_back(m_formulas.get(i));
TRACE("lackr", tout << "infla: " <<mk_ismt2_pp(m_formulas.get(i), m_m, 2) << "\n";);
} }
while (!stack.empty()) { while (!stack.empty()) {