From caa5b0904622d6711cbf1ff328e346f5818eed8b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 22 Apr 2020 13:33:36 -0700
Subject: [PATCH] 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>
---
 src/muz/spacer/spacer_context.cpp | 5 ++---
 src/muz/spacer/spacer_manager.cpp | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index c15506eef..eb59a06d2 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -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;
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 928837c25..61fd9447d 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -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;
 }