From 2f8465552cd05e7f8fd66885c01f40bf9f9b8094 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Thu, 18 Feb 2016 17:08:54 +0000 Subject: [PATCH] additional logging --- src/ackermannization/ackermannize_bv_tactic.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 123b496a1..f9c48c2bd 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -38,6 +38,7 @@ public: tactic_report report("ackermannize", *g); fail_if_unsat_core_generation("ackermannize", g); fail_if_proof_generation("ackermannize", g); + TRACE("ackermannize", g->display(tout << "in\n");); expr_ref_vector flas(m); const unsigned sz = g->size(); @@ -48,6 +49,7 @@ public: goal_ref resg(alloc(goal, *g, true)); const bool success = lackr.mk_ackermann(resg, m_lemma_limit); if (!success) { // Just pass on the input unchanged + TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;); result.reset(); result.push_back(g.get()); mc = 0; @@ -62,7 +64,7 @@ public: } resg->inc_depth(); - TRACE("ackermannize", resg->display(tout);); + TRACE("ackermannize", resg->display(tout << "out\n");); SASSERT(resg->is_well_sorted()); }