diff --git a/src/model/model.cpp b/src/model/model.cpp
index 5d5fa1bd5..06843da5f 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/array_decl_plugin.h"
+#include "ast/bv_decl_plugin.h"
 #include "ast/well_sorted.h"
 #include "ast/used_symbols.h"
 #include "ast/for_each_expr.h"
@@ -410,6 +411,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
     ptr_buffer<expr> args;
     todo.push_back(e);
     array_util autil(m);
+    bv_util bv(m);
     func_interp* fi = nullptr;
     unsigned pid = 0;
     expr_ref new_t(m);
@@ -457,6 +459,10 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
                 var_subst vs(m, false);
                 new_t = vs(fi->get_interp(), args.size(), args.c_ptr());
             }
+            else if (bv.is_bit2bool(t)) {
+                unsigned idx = f->get_parameter(0).get_int();
+                new_t = m.mk_eq(bv.mk_extract(idx, idx, args[0]), bv.mk_numeral(1, 1));
+            }
 #if 0
             else if (is_uninterp_const(a) && !get_const_interp(f)) {
                 new_t = get_some_value(f->get_range());
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index db9af2265..776c4c061 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1121,13 +1121,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
     // adjust result according to model converter.
     unsigned arity = m_head->get_arity();
     model_ref md = alloc(model, m);
-    if (arity == 0) {
-        md->register_decl(m_head, result);
-    } else {
-        func_interp* fi = alloc(func_interp, m, arity);
-        fi->set_else(result);
-        md->register_decl(m_head, fi);
-    }
+    md->register_decl(m_head, result);    
     model_converter_ref mc = ctx.get_model_converter();
     apply(mc, md);
     if (p_orig->get_arity() == 0) {
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index 817d620c9..ae6ab09d8 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -73,7 +73,7 @@ expr_ref inductive_property::fixup_clauses(expr* fml) const
     expr_ref result(m);
     flatten_and(fml, conjs);
     for (unsigned i = 0; i < conjs.size(); ++i) {
-        conjs[i] = fixup_clause(conjs[i].get());
+        conjs[i] = fixup_clause(conjs.get(i));
     }
     bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
     return result;
@@ -83,19 +83,17 @@ std::string inductive_property::to_string() const
 {
     std::stringstream stm;
     model_ref md;
-    expr_ref result(m);
     to_model(md);
-    model_smt2_pp(stm, m, *md.get(), 0);
+    stm << *md;
     return stm.str();
 }
 
-void inductive_property::to_model(model_ref& md) const
-{
+void inductive_property::to_model(model_ref& md) const {
     md = alloc(model, m);
     vector<relation_info> const& rs = m_relation_info;
     expr_ref_vector conjs(m);
-    for (unsigned i = 0; i < rs.size(); ++i) {
-        relation_info ri(rs[i]);
+    for (relation_info const& ri_ : rs) {
+        relation_info ri(ri_);
         func_decl * pred = ri.m_pred;
         expr_ref prop = fixup_clauses(ri.m_body);
         func_decl_ref_vector const& sig = ri.m_vars;
@@ -105,16 +103,11 @@ void inductive_property::to_model(model_ref& md) const
             sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1]));
         }
         expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
-        if (sig.empty()) {
-            md->register_decl(pred, q);
-        } else {
-            func_interp* fi = alloc(func_interp, m, sig.size());
-            fi->set_else(q);
-            md->register_decl(pred, fi);
-        }
+        md->register_decl(pred, q);
     }
-    TRACE("spacer", model_smt2_pp(tout, m, *md, 0););
+    TRACE("spacer", tout << *md;);
     apply(const_cast<model_converter_ref&>(m_mc), md);
+    md->compress();
 }
 
 expr_ref inductive_property::to_expr() const