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

Fix typos

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-25 14:42:18 -07:00
parent def69e2521
commit 9abcde9a35
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

@ -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() {

2
src/tactic/bv/max_bv_sharing_tactic.cpp
View file

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

6
src/tactic/core/propagate_values_tactic.cpp
View file

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