mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

move debug output to before state update

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-11 12:51:46 -08:00
parent f7269bb60a
commit 6a1b3f7344
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -108,7 +108,7 @@ void elim_unconstrained::eliminate() {
else
m_created_compound = true;
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";);
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(get_node(v).m_orig, m) << " " << mk_bounded_pp(t, m) << " -> " << r << " " << get_node(e).m_refcount << "\n";);
SASSERT(!side_cond && "not implemented to add side conditions\n");
}
@ -264,9 +264,9 @@ void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
if (f == g)
continue;
old_fmls.push_back(m_fmls[i]);
m_fmls.update(i, dependent_expr(m, g, nullptr, d));
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
TRACE("elim_unconstrained", tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
m_fmls.update(i, dependent_expr(m, g, nullptr, d));
}
}