mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 14:10:54 +00:00
Code Activity

debug print

Browse source
This commit is contained in:
Arie Gurfinkel 2017-08-07 11:49:43 +02:00
parent 1d478bd8d3
commit 6917aa3eb9
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/muz/spacer/spacer_context.cpp
View file

@ -333,7 +333,18 @@ void pred_transformer::add_lemma_core(lemma* lemma,
STRACE ("spacer.expand-add", STRACE ("spacer.expand-add",
tout << "add-lemma: " << pp_level (lvl) << " " tout << "add-lemma: " << pp_level (lvl) << " "
<< head ()->get_name () << " " << head ()->get_name () << " "
<< mk_epp (l, m) << "\n\n";); << mk_epp (l, m) << "\n";
if (!lemma->is_ground()) {
expr_ref_vector inst(m);
lemma->mk_insts(inst);
for (unsigned i = 0, sz = inst.size(); i < sz; ++i) {
tout << mk_epp(inst.get(i), m) << "\n";
}
}
tout << "\n";
);
if (is_infty_level(lvl)) { m_stats.m_num_invariants++; } if (is_infty_level(lvl)) { m_stats.m_num_invariants++; }
@ -3046,6 +3057,8 @@ bool context::propagate(unsigned min_prop_lvl,
if (m_params.pdr_simplify_formulas_pre()) { if (m_params.pdr_simplify_formulas_pre()) {
simplify_formulas(); simplify_formulas();
} }
STRACE ("spacer.expand-add", tout << "Propagating\n";);
IF_VERBOSE (1, verbose_stream () << "Propagating: " << std::flush;); IF_VERBOSE (1, verbose_stream () << "Propagating: " << std::flush;);
for (unsigned lvl = min_prop_lvl; lvl <= full_prop_lvl; lvl++) { for (unsigned lvl = min_prop_lvl; lvl <= full_prop_lvl; lvl++) {