mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix #4050 - have to delay model compression because it may use internal symbols that have to be transformed. model compression is used prior to displaying certificate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
95a78b2450
commit
caa5b09046
|
@ -2895,8 +2895,7 @@ expr_ref context::get_answer()
|
|||
}
|
||||
}
|
||||
|
||||
expr_ref context::mk_unsat_answer() const
|
||||
{
|
||||
expr_ref context::mk_unsat_answer() const {
|
||||
expr_ref_vector refs(m);
|
||||
vector<relation_info> rs;
|
||||
get_level_property(m_inductive_lvl, refs, rs, use_bg_invs());
|
||||
|
@ -2961,7 +2960,7 @@ expr_ref context::get_ground_sat_answer() const {
|
|||
}
|
||||
|
||||
void context::display_certificate(std::ostream &out) const {
|
||||
switch(m_last_result) {
|
||||
switch (m_last_result) {
|
||||
case l_false:
|
||||
out << mk_pp(mk_unsat_answer(), m);
|
||||
break;
|
||||
|
|
|
@ -99,7 +99,6 @@ void inductive_property::to_model(model_ref& md) const {
|
|||
}
|
||||
TRACE("spacer", tout << *md;);
|
||||
apply(const_cast<model_converter_ref&>(m_mc), md);
|
||||
md->compress();
|
||||
}
|
||||
|
||||
expr_ref inductive_property::to_expr() const
|
||||
|
@ -107,6 +106,7 @@ expr_ref inductive_property::to_expr() const
|
|||
model_ref md;
|
||||
expr_ref result(m);
|
||||
to_model(md);
|
||||
md->compress();
|
||||
model2expr(md, result);
|
||||
return result;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue