mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-03 08:38:06 +00:00
Code Activity

make verbose model only use simplified rules

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-17 15:27:51 -08:00
parent 29a45e34a2
commit 8592f5cef4
3 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/muz_qe/pdr_context.cpp
View file

@ -97,7 +97,6 @@ namespace pdr {
np += m_levels[i].size();
}
st.update("PDR num properties", np);
std::cout << m_stats.m_num_propagations << " " << np << "\n";
}
void pred_transformer::reset_statistics() {
@ -1501,7 +1500,14 @@ namespace pdr {
simplify_formulas();
m_last_result = l_false;
TRACE("pdr", display_certificate(tout););
IF_VERBOSE(1, display_certificate(verbose_stream()););
IF_VERBOSE(1, {
expr_ref_vector refs(m);
vector<relation_info> rs;
get_level_property(m_inductive_lvl, refs, rs);
model_converter_ref mc;
inductive_property ex(m, mc, rs);
verbose_stream() << ex.to_string();
});
validate();
return l_false;
}