From 9abcde9a358f883befbcad910e880263182e5577 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Mar 2013 14:42:18 -0700 Subject: [PATCH] Fix typos Signed-off-by: Leonardo de Moura --- src/smt/asserted_formulas.cpp | 2 +- src/tactic/bv/max_bv_sharing_tactic.cpp | 2 +- src/tactic/core/propagate_values_tactic.cpp | 6 +++--- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3155d9c58..c5d3c08cf 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -653,7 +653,7 @@ void asserted_formulas::propagate_values() { // will be (silently) eliminated, and models produced by Z3 will not contain them. flush_cache(); } - TRACE("propagate_values", tout << "afer:\n"; display(tout);); + TRACE("propagate_values", tout << "after:\n"; display(tout);); } void asserted_formulas::propagate_booleans() { diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 251e2b754..f60487d60 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -269,7 +269,7 @@ class max_bv_sharing_tactic : public tactic { m_rw.cfg().cleanup(); g->inc_depth(); result.push_back(g.get()); - TRACE("qe", g->display(tout);); + TRACE("max_bv_sharing", g->display(tout);); SASSERT(g->is_well_sorted()); } }; diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 6d9e6ccbd..1e358177f 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -165,7 +165,7 @@ class propagate_values_tactic : public tactic { m_occs(*m_goal); while (true) { - TRACE("propagate_values", m_goal->display(tout);); + TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display(tout);); if (forward) { for (; m_idx < size; m_idx++) { process_current(); @@ -201,14 +201,14 @@ class propagate_values_tactic : public tactic { if (round >= m_max_rounds) break; IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;); - TRACE("propgate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";); + TRACE("propagate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";); } end: m_goal->elim_redundancies(); m_goal->inc_depth(); result.push_back(m_goal); SASSERT(m_goal->is_well_sorted()); - TRACE("propagate_values", m_goal->display(tout);); + TRACE("propagate_values", tout << "end\n"; m_goal->display(tout);); TRACE("propagate_values_core", m_goal->display_with_dependencies(tout);); m_goal = 0; }